diff options
| author | barras | 2004-10-20 13:50:08 +0000 |
|---|---|---|
| committer | barras | 2004-10-20 13:50:08 +0000 |
| commit | 9c6487ba87f448daa28158c6e916e3d932c50645 (patch) | |
| tree | 31bc965d5d14b34d4ab501cbd2350d1de44750c5 /tactics/setoid_replace.ml | |
| parent | 1457d6a431755627e3b52eaf74ddd09c641a9fe3 (diff) | |
COMMITED BYTECODE COMPILER
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/setoid_replace.ml')
| -rw-r--r-- | tactics/setoid_replace.ml | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index cf0388543d..a1873770ba 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -690,7 +690,8 @@ let add_morphism lemma_infos mor_name (m,quantifiers_rev,args,output) = [| argsconstr; outputconstr; apply_to_rels m quantifiers_rev ; apply_to_rels mext quantifiers_rev |])); const_entry_type = None; - const_entry_opaque = false}, + const_entry_opaque = false; + const_entry_boxed = false}, IsDefinition)) ; mext in @@ -993,7 +994,8 @@ let int_add_relation id a aeq refl sym trans = Name (id_of_string "X"),None,mkType (Termops.new_univ ())] @ a_quantifiers_rev); const_entry_type = None; - const_entry_opaque = false}, + const_entry_opaque = false; + const_entry_boxed = false}, IsDefinition) in let id_precise = id_of_string (string_of_id id ^ "_precise_relation_class") in let xreflexive_relation_class = @@ -1009,7 +1011,8 @@ let int_add_relation id a aeq refl sym trans = {const_entry_body = Sign.it_mkLambda_or_LetIn xreflexive_relation_class a_quantifiers_rev; const_entry_type = None; - const_entry_opaque = false}, + const_entry_opaque = false; + const_entry_boxed = false }, IsDefinition) in let aeq_rel = { aeq_rel with @@ -1068,7 +1071,8 @@ let int_add_relation id a aeq refl sym trans = (DefinitionEntry {const_entry_body = Sign.it_mkLambda_or_LetIn lemma a_quantifiers_rev; const_entry_type = None; - const_entry_opaque = false}, + const_entry_opaque = false; + const_entry_boxed = false}, IsDefinition) in let a_quantifiers_rev = |