Imported Upstream version 8.0pl2upstream/8.0pl2

12 files changed, 85 insertions, 49 deletions

diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index ad1c4391..0dcdffeb 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: constrextern.mli,v 1.11.2.2 2004/07/16 20:51:12 herbelin Exp $ *)
+(*i $Id: constrextern.mli,v 1.11.2.3 2005/01/21 16:41:50 herbelin Exp $ i*)
 
 (*i*)
 open Util
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index e1b916e1..222ea23b 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: constrintern.ml,v 1.58.2.2 2004/07/16 20:51:12 herbelin Exp $ *)
+(* $Id: constrintern.ml,v 1.58.2.6 2004/11/22 14:21:23 herbelin Exp $ *)
 
 open Pp
 open Util
@@ -154,8 +154,10 @@ let add_glob loc ref =
   i*)
   let sp = Nametab.sp_of_global ref in
   let id = let _,id = repr_path sp in string_of_id id in
-  let dp = string_of_dirpath (Lib.library_part ref) in
-  dump_string (Printf.sprintf "R%d %s.%s\n" (fst (unloc loc)) dp id)
+  let dir = Lib.file_part ref in
+  if dir <> None then
+    let dp = string_of_dirpath (out_some dir) in
+    dump_string (Printf.sprintf "R%d %s.%s\n" (fst (unloc loc)) dp id)
 
 let loc_of_notation f loc args ntn =
   if args=[] or ntn.[0] <> '_' then fst (unloc loc)
@@ -630,6 +632,10 @@ let check_projection isproj nargs r =
   | _, Some _ -> user_err_loc (loc_of_rawconstr r, "", str "Not a projection")
   | _, None -> ()
 
+let get_implicit_name n imps =
+  if !Options.v7 then None
+  else Some (Impargs.name_of_implicit (List.nth imps (n-1)))
+
 let set_hole_implicit i = function
   | RRef (loc,r) -> (loc,ImplicitArg (r,i))
   | RVar (loc,id) -> (loc,ImplicitArg (VarRef id,i))
@@ -680,8 +686,14 @@ let coerce_to_id = function
         str"This expression should be a simple identifier")
 
 let traverse_binder subst id (ids,tmpsc,scopes as env) =
-  let id = try coerce_to_id (fst (List.assoc id subst)) with Not_found -> id in
-  id,(Idset.add id ids,tmpsc,scopes)
+  try
+    (* Binders bound in the notation are consider first-order object *)
+    (* and binders not bound in the notation do not capture variables *)
+    (* outside the notation *)
+    let id' = coerce_to_id (fst (List.assoc id subst)) in
+    id', (Idset.add id' ids,tmpsc,scopes)
+  with Not_found ->
+    id, env
 
 let decode_constrlist_value = function
   | CAppExpl (_,_,l) -> l
@@ -895,7 +907,9 @@ let internalise sigma env allow_soapp lvar c =
 
   and intern_local_binder ((ids,ts,sc as env),bl) = function
       LocalRawAssum(nal,ty) ->
-        let ty = intern_type env ty in
+        let (loc,na) = List.hd nal in
+        (* TODO: fail if several names with different implicit types *)
+        let ty = locate_if_isevar loc na (intern_type env ty) in
         List.fold_left
           (fun ((ids,ts,sc),bl) (_,na) ->
             ((name_fold Idset.add na ids,ts,sc), (na,None,ty)::bl))
@@ -980,7 +994,7 @@ let internalise sigma env allow_soapp lvar c =
 	    (* with implicit arguments *)
 	    []
 	  else
-	    RHole (set_hole_implicit n c) :: 
+	    RHole (set_hole_implicit (n,get_implicit_name n l) c) :: 
 	      aux (n+1) impl' subscopes' eargs rargs
 	  end
       | (imp::impl', a::rargs') ->
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index a65ab6a7..06039da7 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: constrintern.mli,v 1.15.2.1 2004/07/16 19:30:22 herbelin Exp $ *)
+(*i $Id: constrintern.mli,v 1.15.2.2 2005/01/21 16:41:50 herbelin Exp $ i*)
 
 (*i*)
 open Names
@@ -64,7 +64,7 @@ val interp_casted_openconstr    :
 (* [interp_type_with_implicits] extends [interp_type] by allowing
    implicits arguments in the ``rel'' part of [env]; the extra
    argument associates a list of implicit positions to identifiers
-   declared in the rel_context of [env] *)
+   declared in the [rel_context] of [env] *)
 val interp_type_with_implicits : 
   evar_map -> env -> full_implicits_env -> constr_expr -> types
 
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index 7ac2a5c9..3b377f29 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqlib.mli,v 1.5.2.1 2004/07/16 19:30:22 herbelin Exp $ *)
+(*i $Id: coqlib.mli,v 1.5.2.3 2005/01/21 17:14:10 herbelin Exp $ i*)
 
 (*i*)
 open Names
@@ -80,7 +80,7 @@ val build_coq_eq_data : coq_leibniz_eq_data delayed
 val build_coq_eqT_data : coq_leibniz_eq_data delayed
 val build_coq_idT_data : coq_leibniz_eq_data delayed
 
-val build_coq_eq : constr delayed (* = (build_coq_eq_data()).eq *)
+val build_coq_eq : constr delayed (* = [(build_coq_eq_data()).eq] *)
 val build_coq_f_equal2 : constr delayed
 val build_coq_eqT : constr delayed
 val build_coq_sym_eqT : constr delayed
diff --git a/interp/doc.tex b/interp/doc.tex
index 4d60ec34..5bd92fbd 100644
--- a/interp/doc.tex
+++ b/interp/doc.tex
@@ -2,13 +2,13 @@
 \newpage
 \section*{The interpretation of Coq front abstract syntax of terms}
 
-\ocwsection \label{library}
+\ocwsection \label{interp}
 This chapter describes the translation from \Coq\ context-dependent
-front abstract syntax of terms (\verb=front=} to and from the
+front abstract syntax of terms (\verb=front=) to and from the
 context-free, untyped, raw form of constructions (\verb=rawconstr=).
 
 The modules translating back and forth the front abstract syntax are
 organized as follows.
 
 \bigskip
-\begin{center}\epsfig{file=library.dep.ps}\end{center}
+\begin{center}\epsfig{file=interp.dep.ps}\end{center}
diff --git a/interp/genarg.ml b/interp/genarg.ml
index af3d805a..7facebcc 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: genarg.ml,v 1.9.2.1 2004/07/16 19:30:22 herbelin Exp $ *)
+(* $Id: genarg.ml,v 1.9.2.2 2005/01/15 14:56:54 herbelin Exp $ *)
 
 open Pp
 open Util
@@ -34,6 +34,7 @@ type argument_type =
   | ConstrMayEvalArgType
   | QuantHypArgType
   | TacticArgType
+  | OpenConstrArgType
   | CastedOpenConstrArgType
   | ConstrWithBindingsArgType
   | BindingsArgType
@@ -85,8 +86,8 @@ and pr_case_intro_pattern = function
       ++ str "]"
 
 type open_constr = Evd.evar_map * Term.constr
-type open_constr_expr = constr_expr
-type open_rawconstr = rawconstr_and_expr
+type open_constr_expr = unit * constr_expr
+type open_rawconstr = unit * rawconstr_and_expr
 
 let rawwit_bool = BoolArgType
 let globwit_bool = BoolArgType
@@ -144,6 +145,10 @@ let rawwit_tactic = TacticArgType
 let globwit_tactic = TacticArgType
 let wit_tactic = TacticArgType
 
+let rawwit_open_constr = OpenConstrArgType
+let globwit_open_constr = OpenConstrArgType
+let wit_open_constr = OpenConstrArgType
+
 let rawwit_casted_open_constr = CastedOpenConstrArgType
 let globwit_casted_open_constr = CastedOpenConstrArgType
 let wit_casted_open_constr = CastedOpenConstrArgType
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 59b6e10d..967d5050 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: genarg.mli,v 1.9.2.1 2004/07/16 19:30:22 herbelin Exp $ *)
+(*i $Id: genarg.mli,v 1.9.2.4 2005/01/21 17:14:10 herbelin Exp $ i*)
 
 open Util
 open Names
@@ -19,14 +19,14 @@ open Term
 type 'a or_var = ArgArg of 'a | ArgVar of identifier located
 type 'a and_short_name = 'a * identifier located option
 
-(* In globalize tactics, we need to keep the initial constr_expr to recompute*)
+(* In globalize tactics, we need to keep the initial [constr_expr] to recompute*)
 (* in the environment by the effective calls to Intro, Inversion, etc *)
-(* The constr_expr field is None in TacDef though *)
+(* The [constr_expr] field is [None] in TacDef though *)
 type rawconstr_and_expr = rawconstr * constr_expr option
 
 type open_constr = Evd.evar_map * Term.constr
-type open_constr_expr = constr_expr
-type open_rawconstr = rawconstr_and_expr
+type open_constr_expr = unit * constr_expr
+type open_rawconstr = unit * rawconstr_and_expr
 
 type intro_pattern_expr =
   | IntroOrAndPattern of case_intro_pattern_expr
@@ -39,6 +39,7 @@ val pr_case_intro_pattern : case_intro_pattern_expr -> Pp.std_ppcmds
 
 (* The route of a generic argument, from parsing to evaluation
 
+\begin{verbatim}
               parsing        in_raw                           out_raw
     char stream ----> rawtype ----> rawconstr generic_argument ---->
                                                                    |
@@ -46,16 +47,18 @@ val pr_case_intro_pattern : case_intro_pattern_expr -> Pp.std_ppcmds
                                                                    V
                           type  <---- constr generic_argument  <----
                                   out                            in
+\end{verbatim}
 
 To distinguish between the uninterpreted (raw) and the interpreted
-worlds, we annotate the type generic_argument by a phantom argument
-which is either constr_expr or constr (actually we add also a second
-argument raw_tactic_expr and tactic, but this is only for technical
+worlds, we annotate the type [generic_argument] by a phantom argument
+which is either [constr_expr] or [constr] (actually we add also a second
+argument [raw_tactic_expr] and [tactic], but this is only for technical
 reasons, because these types are undefined at the type of compilation
-of Genarg).
+of [Genarg]).
 
 Transformation for each type :
-tag   f                          raw open type          cooked closed type
+\begin{verbatim}
+tag                            raw open type            cooked closed type
 
 BoolArgType                    bool                     bool
 IntArgType                     int                      int
@@ -70,12 +73,13 @@ ConstrArgType                  constr_expr              constr
 ConstrMayEvalArgType           constr_expr may_eval     constr
 QuantHypArgType                quantified_hypothesis    quantified_hypothesis
 TacticArgType                  raw_tactic_expr          tactic
-CastedOpenConstrArgType        constr_expr              open_constr
+OpenConstrArgType              constr_expr              open_constr
 ConstrBindingsArgType      constr_expr with_bindings constr with_bindings
 List0ArgType of argument_type
 List1ArgType of argument_type
 OptArgType of argument_type
 ExtraArgType of string         '_a                      '_b
+\end{verbatim}
 *)
 
 type ('a,'co,'ta) abstract_argument_type
@@ -132,6 +136,10 @@ val rawwit_constr_may_eval : ((constr_expr,reference) may_eval,constr_expr,'ta)
 val globwit_constr_may_eval : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) may_eval,rawconstr_and_expr,'ta) abstract_argument_type
 val wit_constr_may_eval : (constr,constr,'ta) abstract_argument_type
 
+val rawwit_open_constr : (open_constr_expr,constr_expr,'ta) abstract_argument_type
+val globwit_open_constr : (open_rawconstr,rawconstr_and_expr,'ta) abstract_argument_type
+val wit_open_constr : (open_constr,constr,'ta) abstract_argument_type
+
 val rawwit_casted_open_constr : (open_constr_expr,constr_expr,'ta) abstract_argument_type
 val globwit_casted_open_constr : (open_rawconstr,rawconstr_and_expr,'ta) abstract_argument_type
 val wit_casted_open_constr : (open_constr,constr,'ta) abstract_argument_type
@@ -167,7 +175,7 @@ val wit_pair :
   ('b,'co,'ta) abstract_argument_type ->
       ('a * 'b,'co,'ta) abstract_argument_type
 
-(* 'a generic_argument = (Sigma t:type. t[constr/'a]) *)
+(* ['a generic_argument] = (Sigma t:type. t[[constr/'a]]) *)
 type ('a,'b) generic_argument
 
 val fold_list0 : 
@@ -227,6 +235,7 @@ type argument_type =
   | ConstrMayEvalArgType
   | QuantHypArgType
   | TacticArgType
+  | OpenConstrArgType
   | CastedOpenConstrArgType
   | ConstrWithBindingsArgType
   | BindingsArgType
@@ -247,7 +256,7 @@ val unquote : ('a,'co,'ta) abstract_argument_type -> argument_type
 
    with f a = b if a is Constr, f a = c if a is Tactic, otherwise f a = |a|
 
-   in_generic is not typable; we replace the second argument by an absurd
+   [in_generic] is not typable; we replace the second argument by an absurd
    type (with no introduction rule)
 *)
 type an_arg_of_this_type
diff --git a/interp/ppextend.mli b/interp/ppextend.mli
index 056b7a42..bc0a83ec 100644
--- a/interp/ppextend.mli
+++ b/interp/ppextend.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ppextend.mli,v 1.4.2.1 2004/07/16 19:30:22 herbelin Exp $ *)
+(*i $Id: ppextend.mli,v 1.4.2.2 2005/01/21 16:41:50 herbelin Exp $ i*)
 
 (*i*)
 open Pp
diff --git a/interp/symbols.ml b/interp/symbols.ml
index ed151d8e..d1abb084 100644
--- a/interp/symbols.ml
+++ b/interp/symbols.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: symbols.ml,v 1.31.2.1 2004/07/16 19:30:23 herbelin Exp $ *)
+(* $Id: symbols.ml,v 1.31.2.2 2004/11/17 09:33:38 herbelin Exp $ *)
 
 (*i*)
 open Util
@@ -270,7 +270,7 @@ let declare_notation_interpretation ntn scopt pat df pp8only =
   let scope = match scopt with Some s -> s | None -> default_scope in
   let sc = find_scope scope in
   if Stringmap.mem ntn sc.notations && Options.is_verbose () then
-    warning ("Notation "^ntn^" is already used"^
+    warning ("Notation "^ntn^" was already used"^
     (if scopt = None then "" else " in scope "^scope));
   let sc = { sc with notations = Stringmap.add ntn (pat,df,pp8only) sc.notations } in
   scope_map := Stringmap.add scope sc !scope_map;
diff --git a/interp/symbols.mli b/interp/symbols.mli
index 00d8e5ff..5401ae77 100644
--- a/interp/symbols.mli
+++ b/interp/symbols.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: symbols.mli,v 1.22.2.1 2004/07/16 19:30:23 herbelin Exp $ *)
+(*i $Id: symbols.mli,v 1.22.2.3 2005/01/21 17:14:10 herbelin Exp $ i*)
 
 (*i*)
 open Util
@@ -30,7 +30,7 @@ open Ppextend
 type level = precedence * tolerability list
 type delimiters = string
 type scope
-type scopes (* = scope_name list*)
+type scopes (* = [scope_name list] *)
 
 val type_scope : scope_name
 val declare_scope : scope_name -> unit
@@ -52,7 +52,7 @@ val find_delimiters_scope : loc -> delimiters -> scope_name
 
 (*s Declare and uses back and forth a numeral interpretation *)
 
-(* A numeral interpreter is the pair of an interpreter for _integer_
+(* A numeral interpreter is the pair of an interpreter for **integer**
    numbers in terms and an optional interpreter in pattern, if
    negative numbers are not supported, the interpreter must fail with
    an appropriate error message *)
@@ -69,12 +69,12 @@ type required_module = global_reference * string list
 val declare_numeral_interpreter : scope_name -> required_module ->
   num_interpreter -> num_uninterpreter -> unit
 
-(* Returns the term/cases_pattern bound to a numeral in a given scope context*)
+(* Return the [term]/[cases_pattern] bound to a numeral in a given scope context*)
 val interp_numeral : loc -> bigint -> scope_name list -> rawconstr
 val interp_numeral_as_pattern : loc -> bigint -> name -> scope_name list ->
   cases_pattern
 
-(* Returns the numeral bound to a term/cases_pattern; raises No_match if no *)
+(* Return the numeral bound to a [term]/[cases_pattern]; raise [No_match] if no *)
 (* such numeral *)
 val uninterp_numeral : rawconstr -> scope_name * bigint
 val uninterp_cases_numeral : cases_pattern -> scope_name * bigint
@@ -92,11 +92,11 @@ val declare_notation_interpretation : notation -> scope_name option ->
 
 val declare_uninterpretation : interp_rule -> interpretation -> unit
 
-(* Returns the interpretation bound to a notation *)
+(* Return the interpretation bound to a notation *)
 val interp_notation : loc -> notation -> scope_name list -> 
       interpretation * ((dir_path * string) * scope_name option)
 
-(* Returns the possible notations for a given term *)
+(* Return the possible notations for a given term *)
 val uninterp_notations : rawconstr ->
       (interp_rule * interpretation * int option) list
 val uninterp_cases_pattern_notations : cases_pattern ->
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 3ee3285b..a2b6e8b7 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: topconstr.ml,v 1.35.2.2 2004/07/16 19:30:23 herbelin Exp $ *)
+(* $Id: topconstr.ml,v 1.35.2.3 2004/11/17 09:51:41 herbelin Exp $ *)
 
 (*i*)
 open Pp
@@ -89,8 +89,11 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
   | AOrderedCase (b,tyopt,tm,bv) ->
       ROrderedCase (loc,b,option_app (f e) tyopt,f e tm,Array.map (f e) bv,ref None)
   | ALetTuple (nal,(na,po),b,c) ->
+      let e,nal = list_fold_map (fun e na -> let (na,e) = name_app g e na in e,na) e nal in 
+      let na,e = name_app g e na in
       RLetTuple (loc,nal,(na,option_app (f e) po),f e b,f e c)
   | AIf (c,(na,po),b1,b2) ->
+      let na,e = name_app g e na in
       RIf (loc,f e c,(na,option_app (f e) po),f e b1,f e b2)
   | ACast (c,t) -> RCast (loc,f e c,f e t)
   | ASort x -> RSort (loc,x)
@@ -271,8 +274,11 @@ let aconstr_and_vars_of_rawconstr a =
   | ROrderedCase (_,b,tyopt,tm,bv,_) ->
       AOrderedCase (b,option_app aux tyopt,aux tm, Array.map aux bv)
   | RLetTuple (loc,nal,(na,po),b,c) ->
+      add_name bound_binders na;
+      List.iter (add_name bound_binders) nal;
       ALetTuple (nal,(na,option_app aux po),aux b,aux c)
   | RIf (loc,c,(na,po),b1,b2) ->
+      add_name bound_binders na;
       AIf (aux c,(na,option_app aux po),aux b1,aux b2)
   | RCast (_,c,t) -> ACast (aux c,aux t)
   | RSort (_,s) -> ASort s
@@ -349,17 +355,19 @@ let rec alpha_var id1 id2 = function
 
 let alpha_eq_val (x,y) = x = y
 
-let bind_env sigma var v =
+let bind_env alp sigma var v =
   try
     let vvar = List.assoc var sigma in
     if alpha_eq_val (v,vvar) then sigma
     else raise No_match
   with Not_found ->
+    (* Check that no capture of binding variables occur *)
+    if List.exists (fun (id,_) ->occur_rawconstr id v) alp then raise No_match;
     (* TODO: handle the case of multiple occs in different scopes *)
     (var,v)::sigma
 
 let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
-  | r1, AVar id2 when List.mem id2 metas -> bind_env sigma id2 r1
+  | r1, AVar id2 when List.mem id2 metas -> bind_env alp sigma id2 r1
   | RVar (_,id1), AVar id2 when alpha_var id1 id2 alp -> sigma
   | RRef (_,r1), ARef r2 when r1 = r2 -> sigma
   | RPatVar (_,(_,n1)), APatVar n2 when n1=n2 -> sigma
@@ -417,7 +425,7 @@ and match_alist alp metas sigma l1 l2 x iter termin lassoc =
 
 and match_binders alp metas sigma b1 b2 na1 na2 = match (na1,na2) with
   | (Name id1,Name id2) when List.mem id2 metas ->
-      let sigma = bind_env sigma id2 (RVar (dummy_loc,id1)) in 
+      let sigma = bind_env alp sigma id2 (RVar (dummy_loc,id1)) in 
       match_ alp metas sigma b1 b2
   | (Name id1,Name id2) -> match_ ((id1,id2)::alp) metas sigma b1 b2
   | (Anonymous,Anonymous) -> match_  alp metas sigma b1 b2
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index f4a82a3a..54547352 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: topconstr.mli,v 1.23.2.1 2004/07/16 19:30:23 herbelin Exp $ *)
+(*i $Id: topconstr.mli,v 1.23.2.3 2005/01/21 17:14:10 herbelin Exp $ i*)
 
 (*i*)
 open Pp
@@ -23,12 +23,12 @@ open Term
 (* non global expressions such as existential variables also *)
 
 type aconstr =
-  (* Part common to rawconstr and cases_pattern *)
+  (* Part common to [rawconstr] and [cases_pattern] *)
   | ARef of global_reference
   | AVar of identifier
   | AApp of aconstr * aconstr list
   | AList of identifier * identifier * aconstr * aconstr * bool
-  (* Part only in rawconstr *)
+  (* Part only in [rawconstr] *)
   | ALambda of name * aconstr * aconstr
   | AProd of name * aconstr * aconstr
   | ALetIn of name * aconstr * aconstr
@@ -59,7 +59,7 @@ type scope_name = string
 type interpretation = 
     (identifier * (scope_name option * scope_name list)) list * aconstr
 
-val match_aconstr : (* scope_name option -> *) rawconstr -> interpretation ->
+val match_aconstr : (*i scope_name option -> i*) rawconstr -> interpretation ->
       (rawconstr * (scope_name option * scope_name list)) list
 
 (*s Concrete syntax for terms *)