diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/namegen.ml | 4 | ||||
| -rw-r--r-- | pretyping/termops.ml | 16 | ||||
| -rw-r--r-- | pretyping/termops.mli | 16 |
3 files changed, 18 insertions, 18 deletions
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml index e7c9331527..c3c6b205d9 100644 --- a/pretyping/namegen.ml +++ b/pretyping/namegen.ml @@ -131,9 +131,9 @@ let mkProd_or_LetIn_name env b d = mkProd_or_LetIn (name_assumption env d) b let mkLambda_or_LetIn_name env b d = mkLambda_or_LetIn (name_assumption env d)b let it_mkProd_or_LetIn_name env b hyps = - it_mkProd_or_LetIn ~init:b (name_context env hyps) + it_mkProd_or_LetIn b (name_context env hyps) let it_mkLambda_or_LetIn_name env b hyps = - it_mkLambda_or_LetIn ~init:b (name_context env hyps) + it_mkLambda_or_LetIn b (name_context env hyps) (**********************************************************************) (* Fresh names *) diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 17e0522230..d31242aa2b 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -235,18 +235,18 @@ let mkProd_wo_LetIn (na,body,t) c = | None -> mkProd (na, t, c) | Some b -> subst1 b c -let it_mkProd ~init = List.fold_left (fun c (n,t) -> mkProd (n, t, c)) init -let it_mkLambda ~init = List.fold_left (fun c (n,t) -> mkLambda (n, t, c)) init +let it_mkProd init = List.fold_left (fun c (n,t) -> mkProd (n, t, c)) init +let it_mkLambda init = List.fold_left (fun c (n,t) -> mkLambda (n, t, c)) init let it_named_context_quantifier f ~init = List.fold_left (fun c d -> f d c) init -let it_mkProd_or_LetIn = it_named_context_quantifier mkProd_or_LetIn -let it_mkProd_wo_LetIn = it_named_context_quantifier mkProd_wo_LetIn -let it_mkLambda_or_LetIn = it_named_context_quantifier mkLambda_or_LetIn -let it_mkNamedProd_or_LetIn = it_named_context_quantifier mkNamedProd_or_LetIn -let it_mkNamedProd_wo_LetIn = it_named_context_quantifier mkNamedProd_wo_LetIn -let it_mkNamedLambda_or_LetIn = it_named_context_quantifier mkNamedLambda_or_LetIn +let it_mkProd_or_LetIn init = it_named_context_quantifier mkProd_or_LetIn ~init +let it_mkProd_wo_LetIn init = it_named_context_quantifier mkProd_wo_LetIn ~init +let it_mkLambda_or_LetIn init = it_named_context_quantifier mkLambda_or_LetIn ~init +let it_mkNamedProd_or_LetIn init = it_named_context_quantifier mkNamedProd_or_LetIn ~init +let it_mkNamedProd_wo_LetIn init = it_named_context_quantifier mkNamedProd_wo_LetIn ~init +let it_mkNamedLambda_or_LetIn init = it_named_context_quantifier mkNamedLambda_or_LetIn ~init (* *) diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 1346a7f524..385bd3022a 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -49,14 +49,14 @@ val extended_rel_vect : int -> rel_context -> constr array (** iterators/destructors on terms *) val mkProd_or_LetIn : rel_declaration -> types -> types val mkProd_wo_LetIn : rel_declaration -> types -> types -val it_mkProd : init:types -> (name * types) list -> types -val it_mkLambda : init:constr -> (name * types) list -> constr -val it_mkProd_or_LetIn : init:types -> rel_context -> types -val it_mkProd_wo_LetIn : init:types -> rel_context -> types -val it_mkLambda_or_LetIn : init:constr -> rel_context -> constr -val it_mkNamedProd_or_LetIn : init:types -> named_context -> types -val it_mkNamedProd_wo_LetIn : init:types -> named_context -> types -val it_mkNamedLambda_or_LetIn : init:constr -> named_context -> constr +val it_mkProd : types -> (name * types) list -> types +val it_mkLambda : constr -> (name * types) list -> constr +val it_mkProd_or_LetIn : types -> rel_context -> types +val it_mkProd_wo_LetIn : types -> rel_context -> types +val it_mkLambda_or_LetIn : constr -> rel_context -> constr +val it_mkNamedProd_or_LetIn : types -> named_context -> types +val it_mkNamedProd_wo_LetIn : types -> named_context -> types +val it_mkNamedLambda_or_LetIn : constr -> named_context -> constr val it_named_context_quantifier : (named_declaration -> 'a -> 'a) -> init:'a -> named_context -> 'a |