diff options
| author | soubiran | 2007-04-25 15:13:45 +0000 |
|---|---|---|
| committer | soubiran | 2007-04-25 15:13:45 +0000 |
| commit | 40425048feff138e6c67555c7ee94142452d1cae (patch) | |
| tree | b26134c830f386838f219b92a1c8960dd50c4287 /tactics | |
| parent | 2c75beb4e24c91d3ecab07ca9279924205002ada (diff) | |
New keyword "Inline" for Parameters and Axioms for automatic
delta-reduction at fonctor application.
Example:
Module Type S.
Parameter Inline N : Set.
End S.
Module F (X:S).
Definition t := X.N.
End F.
Module M.
Definition N := nat.
End M.
Module G := F M.
Print G.t.
G.t = nat
: Set
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9795 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/setoid_replace.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 1273c65e45..269c40fec3 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -908,7 +908,7 @@ let new_morphism m signature id hook = begin ignore (Declare.declare_internal_constant id - (ParameterEntry lem, IsAssumption Logical)) ; + (ParameterEntry (lem,false), IsAssumption Logical)) ; let mor_name = morphism_theory_id_of_morphism_proof_id id in let lemma_infos = Some (id,argsconstr,outputconstr) in add_morphism lemma_infos mor_name diff --git a/tactics/tactics.ml b/tactics/tactics.ml index c496ffe64b..defb7b7497 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2524,7 +2524,7 @@ let admit_as_an_axiom gls = let concl = it_mkNamedProd_or_LetIn (pf_concl gls) sign in if occur_existential concl then error "\"admit\" cannot handle existentials"; let axiom = - let cd = Entries.ParameterEntry concl in + let cd = Entries.ParameterEntry (concl,false) in let con = Declare.declare_internal_constant na (cd,IsAssumption Logical) in constr_of_global (ConstRef con) in |