← Back to branch summary

~naesten/coq/trunk

« back to all changes in this revision

Viewing changes to pretyping/indrec.ml

  • Committer: herbelin
  • Date: 2009-11-09 18:05:13 UTC
  • Revision ID: svn-v4:85f007b7-540e-0410-9357-904b9bb8a0f7:trunk:12485
A bit of cleaning around name generation + creation of dedicated file namegen.ml

Show diffs side-by-side

added added

removed removed

Lines of Context:
pretyping/indrec.ml
19
19
open Nameops
20
20
open Term
21
21
open Termops
 
22
open Namegen
22
23
open Declarations
23
24
open Entries
24
25
open Inductive
40
41
 
41
42
exception RecursionSchemeError of recursion_scheme_error
42
43
 
43
 
let make_prod_dep dep env = if dep then prod_name env else mkProd
 
44
let make_prod_dep dep env = if dep then mkProd_name env else mkProd
44
45
let mkLambda_string s t c = mkLambda (Name (id_of_string s), t, c)
45
46
 
46
47
(*******************************************)
205
206
      match kind_of_term p' with
206
207
        | Prod (n,t,c) ->
207
208
            let d = (n,None,t) in
208
 
            lambda_name env (n,t,prec (push_rel d env) (i+1) (d::hyps) c)
 
209
            mkLambda_name env (n,t,prec (push_rel d env) (i+1) (d::hyps) c)
209
210
        | LetIn (n,b,t,c) ->
210
211
            let d = (n,Some b,t) in
211
212
            mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::hyps) c)
228
229
        in
229
230
        (match optionpos with
230
231
           | None ->
231
 
               lambda_name env
 
232
               mkLambda_name env
232
233
                 (n,t,process_constr (push_rel d env) (i+1)
233
234
                    (whd_beta Evd.empty (applist (lift 1 f, [(mkRel 1)])))
234
235
                    (cprest,rest))
236
237
               let nF = lift (i+1+decF) f_0 in
237
238
               let env' = push_rel d env in
238
239
               let arg = process_pos env' nF (lift 1 t) in
239
 
               lambda_name env
 
240
               mkLambda_name env
240
241
                 (n,t,process_constr env' (i+1)
241
242
                    (whd_beta Evd.empty (applist (lift 1 f, [(mkRel 1); arg])))
242
243
                    (cprest,rest)))