diff options
| -rw-r--r-- | CHANGES | 2 | ||||
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 1 | ||||
| -rw-r--r-- | doc/refman/RefMan-syn.tex | 15 | ||||
| -rw-r--r-- | interp/notation.ml | 10 | ||||
| -rw-r--r-- | library/lib.ml | 11 | ||||
| -rw-r--r-- | library/lib.mli | 1 | ||||
| -rw-r--r-- | test-suite/output/ArgumentsScope.out | 56 | ||||
| -rw-r--r-- | test-suite/output/ArgumentsScope.v | 29 |
8 files changed, 117 insertions, 8 deletions
@@ -31,7 +31,7 @@ Language Vernacular commands -- Added option Global to "Arguments Scope" for section surviving. (DOC TODO) +- Added option Global to "Arguments Scope" for section surviving. - Added option "Unset Elimination Schemes" to deactivate the automatic generation of elimination schemes. - Modification of the Scheme command so you can ask for the name to be diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index dc7235ae6..6b8834526 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -422,6 +422,7 @@ convertibility into an order inductively defined by: \item if $i \leq j$ then $\WTEGLECONV{\Type(i)}{\Type(j)}$, \item for any $i$, $\WTEGLECONV{\Prop}{\Type(i)}$, \item for any $i$, $\WTEGLECONV{\Set}{\Type(i)}$, +\item $\WTEGLECONV{\Prop}{\Set}$, \item if $\WTEGCONV{T}{U}$ and $\WTELECONV{\Gamma::(x:T)}{T'}{U'}$ then $\WTEGLECONV{\forall~x:T,T'}{\forall~x:U,U'}$. \end{enumerate} diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex index e319bdbb1..22eb0eeae 100644 --- a/doc/refman/RefMan-syn.tex +++ b/doc/refman/RefMan-syn.tex @@ -742,6 +742,21 @@ arguments of {\qualid} are built from a notation, then this notation is interpreted in the scope stack extended by the scopes bound (if any) to these arguments. +\begin{Variants} +\item {\tt Arguments Scope Global} {\qualid} {\tt [ \nelist{\optscope}{} ]} + +This behaves like {\tt Arguments Scope} {\qualid} {\tt [ +\nelist{\optscope}{} ]} but survives when a section is closed instead +of stopping working at section closing. + +\item {\tt Arguments Scope Local} {\qualid} {\tt [ \nelist{\optscope}{} ]} + +This is a synonym of {\tt Arguments Scope} {\qualid} {\tt [ +\nelist{\optscope}{} ]}: if in a section, the effect of the command +stops when the section it belongs to ends. +\end{Variants} + + \SeeAlso The command to show the scopes bound to the arguments of a function is described in Section~\ref{About}. diff --git a/interp/notation.ml b/interp/notation.ml index 424cb93ef..bafce17af 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -464,8 +464,8 @@ let subst_arguments_scope (_,subst,(req,r,scl)) = (ArgsScopeNoDischarge,fst (subst_global subst r),scl) let discharge_arguments_scope (_,(req,r,l)) = - if req = ArgsScopeNoDischarge then None - else Some (req,pop_global_reference r,l) + if req = ArgsScopeNoDischarge or (isVarRef r & Lib.is_in_section r) then None + else Some (req,Lib.discharge_global r,l) let rebuild_arguments_scope (_,(req,r,l)) = match req with @@ -493,8 +493,7 @@ let declare_arguments_scope_gen req r scl = Lib.add_anonymous_leaf (inArgumentsScope (req,r,scl)) let declare_arguments_scope local ref scl = - let req = - if local or isVarRef ref then ArgsScopeNoDischarge else ArgsScopeManual in + let req = if local then ArgsScopeNoDischarge else ArgsScopeManual in declare_arguments_scope_gen req ref scl let find_arguments_scope r = @@ -503,8 +502,7 @@ let find_arguments_scope r = let declare_ref_arguments_scope ref = let t = Global.type_of_global ref in - let req = if isVarRef ref then ArgsScopeNoDischarge else ArgsScopeAuto in - declare_arguments_scope_gen req ref (compute_arguments_scope t) + declare_arguments_scope_gen ArgsScopeAuto ref (compute_arguments_scope t) (********************************) (* Encoding notations as string *) diff --git a/library/lib.ml b/library/lib.ml index bb0ad74ca..4743290ae 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -484,13 +484,22 @@ let section_segment_of_constant con = let section_segment_of_mutual_inductive kn = Names.KNmap.find kn (snd (pi3 (List.hd !sectab))) +let rec list_mem_assoc_in_triple x = function + | [] -> raise Not_found + | (a,_,_)::l -> compare a x = 0 or list_mem_assoc_in_triple x l + let section_instance = function - | VarRef id -> [||] + | VarRef id -> + if list_mem_assoc_in_triple id (pi1 (List.hd !sectab)) then [||] + else raise Not_found | ConstRef con -> Names.Cmap.find con (fst (pi2 (List.hd !sectab))) | IndRef (kn,_) | ConstructRef ((kn,_),_) -> Names.KNmap.find kn (snd (pi2 (List.hd !sectab))) +let is_in_section ref = + try ignore (section_instance ref); true with Not_found -> false + let init_sectab () = sectab := [] let freeze_sectab () = !sectab let unfreeze_sectab s = sectab := s diff --git a/library/lib.mli b/library/lib.mli index 80ce26fc6..c13f7f62d 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -173,6 +173,7 @@ val section_segment_of_constant : Names.constant -> Sign.named_context val section_segment_of_mutual_inductive: Names.mutual_inductive -> Sign.named_context val section_instance : Libnames.global_reference -> Names.identifier array +val is_in_section : Libnames.global_reference -> bool val add_section_variable : Names.identifier -> bool -> Term.types option -> unit val add_section_constant : Names.constant -> Sign.named_context -> unit diff --git a/test-suite/output/ArgumentsScope.out b/test-suite/output/ArgumentsScope.out new file mode 100644 index 000000000..6643c1429 --- /dev/null +++ b/test-suite/output/ArgumentsScope.out @@ -0,0 +1,56 @@ +a : bool -> bool + +Argument scope is [bool_scope] +Expands to: Variable a +b : bool -> bool + +Argument scope is [bool_scope] +Expands to: Variable b +negb'' : bool -> bool + +Argument scope is [bool_scope] +negb'' is transparent +Expands to: Constant Top.A.B.negb'' +negb' : bool -> bool + +Argument scope is [bool_scope] +negb' is transparent +Expands to: Constant Top.A.negb' +negb : bool -> bool + +Argument scope is [bool_scope] +negb is transparent +Expands to: Constant Coq.Init.Datatypes.negb +a : bool -> bool + +Expands to: Variable a +b : bool -> bool + +Expands to: Variable b +negb : bool -> bool + +negb is transparent +Expands to: Constant Coq.Init.Datatypes.negb +negb' : bool -> bool + +negb' is transparent +Expands to: Constant Top.A.negb' +negb'' : bool -> bool + +negb'' is transparent +Expands to: Constant Top.A.B.negb'' +a : bool -> bool + +Expands to: Variable a +negb : bool -> bool + +negb is transparent +Expands to: Constant Coq.Init.Datatypes.negb +negb' : bool -> bool + +negb' is transparent +Expands to: Constant Top.negb' +negb'' : bool -> bool + +negb'' is transparent +Expands to: Constant Top.negb'' diff --git a/test-suite/output/ArgumentsScope.v b/test-suite/output/ArgumentsScope.v new file mode 100644 index 000000000..13b5e13dd --- /dev/null +++ b/test-suite/output/ArgumentsScope.v @@ -0,0 +1,29 @@ +(* A few tests to check Argument Scope Global command *) + +Section A. +Variable a : bool -> bool. +Definition negb' := negb. +Section B. +Variable b : bool -> bool. +Definition negb'' := negb. +About a. +About b. +About negb''. +About negb'. +About negb. +Arguments Scope Global negb'' [ _ ]. +Arguments Scope Global negb' [ _ ]. +Arguments Scope Global negb [ _ ]. +Arguments Scope Global a [ _ ]. +Arguments Scope Global b [ _ ]. +About a. +About b. +About negb. +About negb'. +About negb''. +End B. +About a. +End A. +About negb. +About negb'. +About negb''. |