diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-01-28 23:07:59 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-01-28 23:07:59 +0000 |
| commit | 35180e3a927d4450406ebeb0e89fdcde1341650a (patch) | |
| tree | 7fe926a33569320b25c1fa972904354b067061ea /tactics/setoid_replace.ml | |
| parent | adadd8db0e9eb1e5161057a7064426b84a3d2605 (diff) | |
Réorganisation de la structure interne des types de déclarations (decl_kinds)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7941 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/setoid_replace.ml')
| -rw-r--r-- | tactics/setoid_replace.ml | 10 |
1 files changed, 5 insertions, 5 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 |