diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 22 | ||||
| -rw-r--r-- | proofs/goal.ml | 8 | ||||
| -rw-r--r-- | proofs/goal.mli | 4 | ||||
| -rw-r--r-- | proofs/logic.ml | 2 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 4 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 1 |
6 files changed, 25 insertions, 16 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index d25ae38c53..b7ccd647b5 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -577,7 +577,7 @@ let pr_clenv clenv = h 0 (str"TEMPL: " ++ Termops.Internal.print_constr_env clenv.env clenv.evd clenv.templval.rebus ++ str" : " ++ Termops.Internal.print_constr_env clenv.env clenv.evd clenv.templtyp.rebus ++ fnl () ++ - pr_evar_map (Some 2) clenv.evd) + pr_evar_map (Some 2) clenv.env clenv.evd) (****************************************************************) (** Evar version of mk_clenv *) @@ -603,12 +603,20 @@ let make_evar_clause env sigma ?len t = in (** FIXME: do the renaming online *) let t = rename_bound_vars_as_displayed sigma Id.Set.empty [] t in - let rec clrec (sigma, holes) n t = + let rec clrec (sigma, holes) inst n t = if n = 0 then (sigma, holes, t) else match EConstr.kind sigma t with - | Cast (t, _, _) -> clrec (sigma, holes) n t + | Cast (t, _, _) -> clrec (sigma, holes) inst n t | Prod (na, t1, t2) -> - let (sigma, ev) = new_evar env sigma ~typeclass_candidate:false t1 in + (** Share the evar instances as we are living in the same context *) + let inst, ctx, args, subst = match inst with + | None -> + (** Dummy type *) + let ctx, _, args, subst = push_rel_context_to_named_context env sigma mkProp in + Some (ctx, args, subst), ctx, args, subst + | Some (ctx, args, subst) -> inst, ctx, args, subst + in + let (sigma, ev) = new_evar_instance ~typeclass_candidate:false ctx sigma (csubst_subst subst t1) args in let dep = not (noccurn sigma 1 t2) in let hole = { hole_evar = ev; @@ -618,11 +626,11 @@ let make_evar_clause env sigma ?len t = hole_name = na; } in let t2 = if dep then subst1 ev t2 else t2 in - clrec (sigma, hole :: holes) (pred n) t2 - | LetIn (na, b, _, t) -> clrec (sigma, holes) n (subst1 b t) + clrec (sigma, hole :: holes) inst (pred n) t2 + | LetIn (na, b, _, t) -> clrec (sigma, holes) inst n (subst1 b t) | _ -> (sigma, holes, t) in - let (sigma, holes, t) = clrec (sigma, []) bound t in + let (sigma, holes, t) = clrec (sigma, []) None bound t in let holes = List.rev holes in let clause = { cl_concl = t; cl_holes = holes } in (sigma, clause) diff --git a/proofs/goal.ml b/proofs/goal.ml index 4e540de538..7245d4a004 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -72,18 +72,18 @@ module V82 = struct (evk, ev, evars) (* Instantiates a goal with an open term *) - let partial_solution sigma evk c = + let partial_solution env sigma evk c = (* Check that the goal itself does not appear in the refined term *) let _ = if not (Evarutil.occur_evar_upto sigma evk c) then () - else Pretype_errors.error_occur_check Environ.empty_env sigma evk c + else Pretype_errors.error_occur_check env sigma evk c in Evd.define evk c sigma (* Instantiates a goal with an open term, using name of goal for evk' *) - let partial_solution_to sigma evk evk' c = + let partial_solution_to env sigma evk evk' c = let id = Evd.evar_ident evk sigma in - let sigma = partial_solution sigma evk c in + let sigma = partial_solution env sigma evk c in match id with | None -> sigma | Some id -> Evd.rename evk' id sigma diff --git a/proofs/goal.mli b/proofs/goal.mli index 3b31cff8d7..af9fb662bf 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -48,11 +48,11 @@ module V82 : sig goal * EConstr.constr * Evd.evar_map (* Instantiates a goal with an open term *) - val partial_solution : Evd.evar_map -> goal -> EConstr.constr -> Evd.evar_map + val partial_solution : Environ.env -> Evd.evar_map -> goal -> EConstr.constr -> Evd.evar_map (* Instantiates a goal with an open term, reusing name of goal for second goal *) - val partial_solution_to : Evd.evar_map -> goal -> goal -> EConstr.constr -> Evd.evar_map + val partial_solution_to : Environ.env -> Evd.evar_map -> goal -> goal -> EConstr.constr -> Evd.evar_map (* Principal part of the progress tactical *) val progress : goal list Evd.sigma -> goal Evd.sigma -> bool diff --git a/proofs/logic.ml b/proofs/logic.ml index 254c93d0a2..b8612cd2c0 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -590,5 +590,5 @@ let prim_refiner r sigma goal = check_meta_variables env sigma c; let (sgl,cl',sigma,oterm) = mk_refgoals sigma goal [] cl c in let sgl = List.rev sgl in - let sigma = Goal.V82.partial_solution sigma goal (EConstr.of_constr oterm) in + let sigma = Goal.V82.partial_solution env sigma goal (EConstr.of_constr oterm) in (sgl, sigma) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 388bf8efb5..231a8fe266 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -130,10 +130,10 @@ let db_pr_goal sigma g = str" " ++ pc) ++ fnl () let pr_gls gls = - hov 0 (pr_evar_map (Some 2) (sig_sig gls) ++ fnl () ++ db_pr_goal (project gls) (sig_it gls)) + hov 0 (pr_evar_map (Some 2) (pf_env gls) (sig_sig gls) ++ fnl () ++ db_pr_goal (project gls) (sig_it gls)) let pr_glls glls = - hov 0 (pr_evar_map (Some 2) (sig_sig glls) ++ fnl () ++ + hov 0 (pr_evar_map (Some 2) (Global.env()) (sig_sig glls) ++ fnl () ++ prlist_with_sep fnl (db_pr_goal (project glls)) (sig_it glls)) (* Variants of [Tacmach] functions built with the new proof engine *) diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index f302960870..14c83a6802 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -83,6 +83,7 @@ val refine : constr -> tactic (** {6 Pretty-printing functions (debug only). } *) val pr_gls : goal sigma -> Pp.t val pr_glls : goal list sigma -> Pp.t +[@@ocaml.deprecated "Please move to \"new\" proof engine"] (** Variants of [Tacmach] functions built with the new proof engine *) module New : sig |