diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/setoid_replace.ml | 10 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 5 | ||||
| -rw-r--r-- | tactics/tactics.ml | 2 |
3 files changed, 9 insertions, 8 deletions
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index cc58983bd..50261ed97 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -688,7 +688,7 @@ let add_morphism lemma_infos mor_name (m,quantifiers_rev,args,output) = const_entry_type = None; const_entry_opaque = false; const_entry_boxed = Options.boxed_definitions()}, - IsDefinition)) ; + IsDefinition Definition)) ; mext in let mmor = current_constant mor_name in @@ -926,7 +926,7 @@ let new_morphism m signature id hook = begin new_edited id (m,args_ty_quantifiers_rev,args,argsconstr,output,outputconstr); - Pfedit.start_proof id (IsGlobal (Proof Lemma)) + Pfedit.start_proof id (Global, Proof Lemma) (Declare.clear_proofs (Global.named_context ())) lem hook; Options.if_verbose msg (Printer.pr_open_subgoals ()); @@ -1047,7 +1047,7 @@ let int_add_relation id a aeq refl sym trans = const_entry_type = None; const_entry_opaque = false; const_entry_boxed = Options.boxed_definitions()}, - IsDefinition) in + IsDefinition Definition) in let id_precise = id_of_string (string_of_id id ^ "_precise_relation_class") in let xreflexive_relation_class = let subst = @@ -1064,7 +1064,7 @@ let int_add_relation id a aeq refl sym trans = const_entry_type = None; const_entry_opaque = false; const_entry_boxed = Options.boxed_definitions() }, - IsDefinition) in + IsDefinition Definition) in let aeq_rel = { aeq_rel with rel_X_relation_class = current_constant id; @@ -1124,7 +1124,7 @@ let int_add_relation id a aeq refl sym trans = const_entry_type = None; const_entry_opaque = false; const_entry_boxed = Options.boxed_definitions()}, - IsDefinition) + IsDefinition Definition) in let a_quantifiers_rev = List.map (fun (n,b,t) -> assert (b = None); n,t) a_quantifiers_rev in diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 7eff2b69f..aa36074d2 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1175,7 +1175,8 @@ let solvable_by_tactic env evi (ev,args) src = Environ.named_context_of_val evi.evar_hyps = Environ.named_context env -> let id = id_of_string "H" in - start_proof id IsLocal evi.evar_hyps evi.evar_concl (fun _ _ -> ()); + start_proof id (Local,Proof Lemma) evi.evar_hyps evi.evar_concl + (fun _ _ -> ()); begin try by (tclCOMPLETE tac); @@ -1520,7 +1521,7 @@ and interp_letin ist gl = function try let t = tactic_of_value v in let ndc = Environ.named_context_val env in - start_proof id IsLocal ndc typ (fun _ _ -> ()); + start_proof id (Local,Proof Lemma) ndc typ (fun _ _ -> ()); by t; let (_,({const_entry_body = pft},_,_)) = cook_proof () in delete_proof (dummy_loc,id); diff --git a/tactics/tactics.ml b/tactics/tactics.ml index f57b490fc..bbc359ef0 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1816,7 +1816,7 @@ let abstract_subproof name tac gls = if occur_existential concl then error "\"abstract\" cannot handle existentials"; let lemme = - start_proof na (IsGlobal (Proof Lemma)) secsign concl (fun _ _ -> ()); + start_proof na (Global, Proof Lemma) secsign concl (fun _ _ -> ()); let _,(const,kind,_) = try by (tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac)); |