diff options
author | 2009-02-01 00:54:43 +0100 | |
---|---|---|
committer | 2009-02-01 00:54:43 +0100 | |
commit | 9c775561f67ac558c2c408cfa873544e2fea7b0a (patch) | |
tree | 375ac16822f815477b36d50e49bb3cd9633aaa84 /contrib/subtac/subtac_command.ml | |
parent | 3e6a1167fd397f2c72b48315e5d82f6c7e24703f (diff) | |
parent | cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (diff) |
Merge commit 'upstream/8.2.rc2+dfsg'
Diffstat (limited to 'contrib/subtac/subtac_command.ml')
-rw-r--r-- | contrib/subtac/subtac_command.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml index a2f54b02..4876b065 100644 --- a/contrib/subtac/subtac_command.ml +++ b/contrib/subtac/subtac_command.ml @@ -99,7 +99,7 @@ let interp_binder sigma env na t = SPretyping.pretype_gen sigma env ([], []) IsType (locate_if_isevar (loc_of_rawconstr t) na t) let interp_context_evars evdref env params = - let bl = Constrintern.intern_context (Evd.evars_of !evdref) env params in + let bl = Constrintern.intern_context false (Evd.evars_of !evdref) env params in let (env, par, _, impls) = List.fold_left (fun (env,params,n,impls) (na, k, b, t) -> @@ -284,7 +284,7 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = mkApp (constr_of_global (Lazy.force fix_sub_ref), [| argtyp ; wf_rel ; - make_existential dummy_loc ~opaque:false env isevars wf_proof ; + make_existential dummy_loc ~opaque:(Define false) env isevars wf_proof ; lift lift_cst prop ; lift lift_cst intern_body_lam |]) | Some f -> @@ -385,7 +385,7 @@ let interp_recursive fixkind l boxed = let env_rec = push_named_context rec_sign env in (* Get interpretation metadatas *) - let impls = Command.compute_interning_datas env [] fixnames fixtypes fiximps in + let impls = Command.compute_interning_datas env Constrintern.Recursive [] fixnames fixtypes fiximps in let notations = List.fold_right Option.List.cons ntnl [] in (* Interp bodies with rollback because temp use of notations/implicit *) |