diff options
| author | vsiles | 2010-09-02 16:38:36 +0000 |
|---|---|---|
| committer | vsiles | 2010-09-02 16:38:36 +0000 |
| commit | 93383861409291653f393f949e12e5604951dadc (patch) | |
| tree | 0ebdc0c6d1e53effce0ae2d86735b6d20189d69c /tactics | |
| parent | 51b0246d286fba37019af058fc484369bcabf7f9 (diff) | |
* removed declare_constant and declare_internal_constant
(declare_constant_gen was not exported, leading to a lot of silly tests
before calling those functions) and replaced them by
declare_constant : ?internal:internal_flat -> ...
declare_constant's default behaviour is the same as the old declare_constant.
* fixed the default behaviour of inductive scheme failure during coq's
compilation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13395 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/rewrite.ml4 | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index c792367c3b..0e9281a21d 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -1464,7 +1464,7 @@ let add_morphism_infer glob m n = let instance_id = add_suffix n "_Proper" in let instance = build_morphism_signature m in if Lib.is_modtype () then - let cst = Declare.declare_internal_constant instance_id + let cst = Declare.declare_constant ~internal:Declare.KernelSilent instance_id (Entries.ParameterEntry (instance,false), Decl_kinds.IsAssumption Decl_kinds.Logical) in add_instance (Typeclasses.new_instance (Lazy.force proper_class) None glob (ConstRef cst)); diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 2069cc23f3..b253b2375e 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3473,7 +3473,7 @@ let abstract_subproof id tac gl = let const = Pfedit.build_constant_by_tactic secsign concl (tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac)) in let cd = Entries.DefinitionEntry const in - let lem = mkConst (Declare.declare_internal_constant id (cd,IsProof Lemma)) in + let lem = mkConst (Declare.declare_constant ~internal:Declare.KernelSilent id (cd,IsProof Lemma)) in exact_no_check (applist (lem,List.rev (Array.to_list (instance_from_named_context sign)))) gl @@ -3503,7 +3503,7 @@ let admit_as_an_axiom gl = if occur_existential concl then error"\"admit\" cannot handle existentials."; let axiom = let cd = Entries.ParameterEntry (concl,false) in - let con = Declare.declare_internal_constant na (cd,IsAssumption Logical) in + let con = Declare.declare_constant ~internal:Declare.KernelSilent na (cd,IsAssumption Logical) in constr_of_global (ConstRef con) in exact_no_check |