diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml | 8 | ||||
| -rw-r--r-- | tactics/eqschemes.ml | 12 | ||||
| -rw-r--r-- | tactics/ind_tables.ml | 4 | ||||
| -rw-r--r-- | tactics/leminv.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 45 |
5 files changed, 16 insertions, 55 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 9f66248897..0260460e64 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -966,14 +966,15 @@ module Search = struct top_sort evm' goals else List.map (fun (ev, _) -> ev) (Evar.Map.bindings goals) in - let fgoals = Evd.future_goals evm in - let pgoal = Evd.principal_future_goal evm in + let fgoals = Evd.save_future_goals evm in let _, pv = Proofview.init evm' [] in let pv = Proofview.unshelve goals pv in try let (), pv', (unsafe, shelved, gaveup), _ = Proofview.apply env tac pv in + if not (List.is_empty gaveup) then + CErrors.anomaly (Pp.str "run_on_evars not assumed to apply tactics generating given up goals."); if Proofview.finished pv' then let evm' = Proofview.return pv' in assert(Evd.fold_undefined (fun ev _ acc -> @@ -983,7 +984,8 @@ module Search = struct (str "leaking evar " ++ int (Evar.repr ev) ++ spc () ++ pr_ev evm' ev); acc && okev) evm' true); - let evm' = Evd.restore_future_goals evm' (shelved @ fgoals) pgoal in + let fgoals = Evd.shelve_on_future_goals shelved fgoals in + let evm' = Evd.restore_future_goals evm' fgoals in let evm' = evars_reset_evd ~with_conv_pbs:true ~with_univs:false evm' evm in Some evm' else raise Not_found diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 45926551b4..477de6452e 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -214,7 +214,7 @@ let build_sym_scheme env ind = rel_vect (2*nrealargs+2) nrealargs])), mkRel 1 (* varH *), [|cstr (nrealargs+1)|])))) - in c, Evd.evar_universe_context_of ctx + in c, UState.of_context_set ctx let sym_scheme_kind = declare_individual_scheme_object "_sym_internal" @@ -285,7 +285,7 @@ let build_sym_involutive_scheme env ind = mkRel 1|])), mkRel 1 (* varH *), [|mkApp(eqrefl,[|applied_ind_C;cstr (nrealargs+1)|])|])))) - in (c, Evd.evar_universe_context_of ctx), eff + in (c, UState.of_context_set ctx), eff let sym_involutive_scheme_kind = declare_individual_scheme_object "_sym_involutive" @@ -439,7 +439,7 @@ let build_l2r_rew_scheme dep env ind kind = [|main_body|]) else main_body)))))) - in (c, Evd.evar_universe_context_of ctx), + in (c, UState.of_context_set ctx), Safe_typing.concat_private eff' eff (**********************************************************************) @@ -528,7 +528,7 @@ let build_l2r_forward_rew_scheme dep env ind kind = (if dep then realsign_ind_P 1 applied_ind_P' else realsign_P 2) s) (mkNamedLambda varHC applied_PC' (mkVar varHC))|]))))) - in c, Evd.evar_universe_context_of ctx + in c, UState.of_context_set ctx (**********************************************************************) (* Build the right-to-left rewriting lemma for hypotheses associated *) @@ -601,7 +601,7 @@ let build_r2l_forward_rew_scheme dep env ind kind = lift (nrealargs+3) applied_PC, mkRel 1)|]), [|mkVar varHC|])))))) - in c, Evd.evar_universe_context_of ctx + in c, UState.of_context_set ctx (**********************************************************************) (* This function "repairs" the non-dependent r2l forward rewriting *) @@ -808,7 +808,7 @@ let build_congr env (eq,refl,ctx) ind = [|mkApp (refl, [|mkVar varB; mkApp (mkVar varf, [|lift (mip.mind_nrealargs+3) b|])|])|])))))) - in c, Evd.evar_universe_context_of ctx + in c, UState.of_context_set ctx let congr_scheme_kind = declare_individual_scheme_object "_congr" (fun _ ind -> diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index b960a845ce..62ead57f38 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -122,8 +122,8 @@ let compute_name internal id = let define internal id c p univs = let fd = declare_constant ~internal in let id = compute_name internal id in - let ctx = Evd.normalize_evar_universe_context univs in - let c = Universes.subst_opt_univs_constr (Evd.evar_universe_context_subst ctx) c in + let ctx = UState.minimize univs in + let c = Universes.subst_opt_univs_constr (UState.subst ctx) c in let univs = if p then Polymorphic_const_entry (UState.context ctx) else Monomorphic_const_entry (UState.context_set ctx) diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 655283c204..a4cdc1592a 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -218,7 +218,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = end in let avoid = ref Id.Set.empty in let _,_,_,_,sigma = Proof.proof pf in - let sigma = Evd.nf_constraints sigma in + let sigma = Evd.minimize_universes sigma in let rec fill_holes c = match EConstr.kind sigma c with | Evar (e,args) -> diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 20ada48a10..12aef852d0 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -15,7 +15,6 @@ open CErrors open Util open Names open Nameops -open Term open Constr open Termops open Environ @@ -1326,46 +1325,6 @@ let index_of_ind_arg sigma t = | None -> error "Could not find inductive argument of elimination scheme." in aux None 0 t -let enforce_prop_bound_names rename tac = - let open Context.Rel.Declaration in - match rename with - | Some (isrec,nn) when Namegen.use_h_based_elimination_names () -> - (* Rename dependent arguments in Prop with name "H" *) - (* so as to avoid having hypothesis such as "t:True", "n:~A" when calling *) - (* elim or induction with schemes built by Indrec.build_induction_scheme *) - let rec aux env sigma i t = - if i = 0 then t else match EConstr.kind sigma t with - | Prod (Name _ as na,t,t') -> - let very_standard = true in - let na = - if Retyping.get_sort_family_of env sigma t = InProp then - (* "very_standard" says that we should have "H" names only, but - this would break compatibility even more... *) - let s = match Namegen.head_name sigma t with - | Some id when not very_standard -> Id.to_string id - | _ -> "" in - Name (add_suffix Namegen.default_prop_ident s) - else - na in - mkProd (na,t,aux (push_rel (LocalAssum (na,t)) env) sigma (i-1) t') - | Prod (Anonymous,t,t') -> - mkProd (Anonymous,t,aux (push_rel (LocalAssum (Anonymous,t)) env) sigma (i-1) t') - | LetIn (na,c,t,t') -> - mkLetIn (na,c,t,aux (push_rel (LocalDef (na,c,t)) env) sigma (i-1) t') - | _ -> assert false in - let rename_branch i = - Proofview.Goal.enter begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = Tacmach.New.project gl in - let t = Proofview.Goal.concl gl in - change_concl (aux env sigma i t) - end in - (if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn) - tac - (Array.map rename_branch nn) - | _ -> - tac - let rec contract_letin_in_lam_header sigma c = match EConstr.kind sigma c with | Lambda (x,t,c) -> mkLambda (x,t,contract_letin_in_lam_header sigma c) @@ -1386,7 +1345,7 @@ let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags (str "The type of elimination clause is not well-formed.")) in let elimclause' = clenv_fchain ~flags indmv elimclause indclause in - enforce_prop_bound_names rename (Clenvtac.res_pf elimclause' ~with_evars ~with_classes ~flags) + Clenvtac.res_pf elimclause' ~with_evars ~with_classes ~flags end (* @@ -4208,7 +4167,7 @@ let induction_tac with_evars params indvars elim = let elimclause' = recolle_clenv i params indvars elimclause gl in (* one last resolution (useless?) *) let resolved = clenv_unique_resolver ~flags:(elim_flags ()) elimclause' gl in - enforce_prop_bound_names rename (Clenvtac.clenv_refine with_evars resolved) + Clenvtac.clenv_refine with_evars resolved end (* Apply induction "in place" taking into account dependent |