diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-13 18:01:16 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-13 18:01:16 +0000 |
| commit | 79b6291ccda61f631aa2cfec9a12d6ea2a34fa96 (patch) | |
| tree | 1c0462389248e1ecb4a9071add18c87d9648c6f1 /toplevel/command.ml | |
| parent | a74338cc598b5fb45e2cc148d243433500bb5294 (diff) | |
Modules and ppvernac, sequel of Enrico's commit 16261
After some investigation, I see no reason to try to hack
the nametab in ppvernac, since everything happens there
at a lower level (constr_expr). So the offending code that
Enrico protected with a State.with_state_protection is now gone.
By the way, moved some types from Declaremods to Vernacexpr
to avoid some dependencies
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16300 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 0b2e6b352..f8230d63d 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -34,6 +34,7 @@ open Evarutil open Evarconv open Indschemes open Misctypes +open Vernacexpr let rec under_binders env f n c = if Int.equal n 0 then f env Evd.empty c else @@ -188,7 +189,12 @@ let declare_assumption is_coe (local,kind) c imps impl nl (_,ident) = match loca true | Global | Local | Discharge -> let local = get_locality ident local in - let decl = (ParameterEntry (None,c,nl), IsAssumption kind) in + let inl = match nl with + | NoInline -> None + | DefaultInline -> Some (Flags.get_inline_level()) + | InlineAt i -> Some i + in + let decl = (ParameterEntry (None,c,inl), IsAssumption kind) in let kn = declare_constant ident ~local decl in let gr = ConstRef kn in let () = maybe_declare_manual_implicits false gr imps in @@ -386,8 +392,6 @@ let declare_mutual_inductive_with_eliminations isrecord mie impls = declare_default_schemes mind; mind -open Vernacexpr - type one_inductive_impls = Impargs.manual_explicitation list (* for inds *)* Impargs.manual_explicitation list list (* for constrs *) |