diff options
| author | Hugo Herbelin | 2014-08-20 22:30:37 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-09-12 10:39:33 +0200 |
| commit | b006f10e7d591417844ffa1f04eeb926d6092d7b (patch) | |
| tree | 9253b32cb1adabafce28f123ef9eb11d4fa122f4 /plugins/funind/indfun.ml | |
| parent | ca300977724a6b065a98c025d400c71f41b9df4b (diff) | |
Uniformisation of the order of arguments env and sigma.
Diffstat (limited to 'plugins/funind/indfun.ml')
| -rw-r--r-- | plugins/funind/indfun.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index e2273972e7..cd35a09a1d 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -130,7 +130,7 @@ let rec abstract_glob_constr c = function List.fold_right (fun x b -> Constrexpr_ops.mkLambdaC([x],k,t,b)) idl (abstract_glob_constr c bl) -let interp_casted_constr_with_implicits sigma env impls c = +let interp_casted_constr_with_implicits env sigma impls c = Constrintern.intern_gen Pretyping.WithoutTypeConstraint env ~impls ~allow_patvar:false c @@ -148,7 +148,7 @@ let build_newrecursive List.fold_left (fun (env,impls) ((_,recname),bl,arityc,_) -> let arityc = Constrexpr_ops.prod_constr_expr arityc bl in - let arity,ctx = Constrintern.interp_type sigma env0 arityc in + let arity,ctx = Constrintern.interp_type env0 sigma arityc in let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity [] in (Environ.push_named (recname,None,arity) env, Id.Map.add recname impl impls)) (env0,Constrintern.empty_internalization_env) lnameargsardef in @@ -157,7 +157,7 @@ let build_newrecursive let f (_,bl,_,def) = let def = abstract_glob_constr def bl in interp_casted_constr_with_implicits - sigma rec_sign rec_impls def + rec_sign sigma rec_impls def in States.with_state_protection (List.map f) lnameargsardef in |