Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; améliorations diverses de l'affichage; affinement de la syntaxe et des options de Notation; branchement de Syntactic Definition sur Notation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3270 85f007b7-540e-0410-9357-904b9bb8a0f7

7 files changed, 531 insertions, 246 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 0ae4c2214c..c813cf71d1 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -39,9 +39,6 @@ let print_arguments = ref false
 (* If true, prints local context of evars, whatever print_arguments *)
 let print_evar_arguments = ref false
 
-(* This forces printing of cast nodes *)
-let print_casts = ref true
-
 (* This governs printing of implicit arguments.  When
    [print_implicits] is on then [print_implicits_explicit_args] tells
    how implicit args are printed. If on, implicit args are printed
@@ -56,6 +53,8 @@ let print_coercions = ref false
 (* This forces printing universe names of Type{.} *)
 let print_universes = ref false
 
+(* This suppresses printing of numeral and symbols *)
+let print_no_symbol = ref false
 
 let with_option o f x =
   let old = !o in o:=true;
@@ -63,10 +62,23 @@ let with_option o f x =
   with e -> o := old; raise e
 
 let with_arguments f = with_option print_arguments f
-let with_casts f = with_option print_casts f
 let with_implicits f = with_option print_implicits f
 let with_coercions f = with_option print_coercions f
 let with_universes f = with_option print_universes f
+let without_symbols f = with_option print_no_symbol f
+
+(**********************************************************************)
+(* Various externalisation functions *)
+
+let insert_delimiters e = function
+  | None -> e
+  | Some sc -> CDelimiters (dummy_loc,sc,e)
+
+let insert_pat_delimiters e = function
+  | None -> e
+  | Some sc -> CPatDelimiters (dummy_loc,sc,e)
+
+let loc = dummy_loc (* shorter... *)
 
 (**********************************************************************)
 (* conversion of references                                           *)
@@ -90,13 +102,21 @@ let extern_evar loc n = warning "No notation for Meta"; CMeta (loc,n)
 let extern_ref r = Qualid (dummy_loc,shortest_qualid_of_global None r)
 
 (**********************************************************************)
-(* conversion of patterns                                             *)
-
-let rec extern_cases_pattern = function   (* loc is thrown away for printing *)
-  | PatVar (loc,Name id) -> CPatAtom (loc,Some (Ident (loc,id)))
-  | PatVar (loc,Anonymous) -> CPatAtom (loc, None) 
-  | PatCstr(loc,cstrsp,args,na) ->
-      let args = List.map extern_cases_pattern args in
+(* conversion of terms and cases patterns                             *)
+
+let rec extern_cases_pattern_in_scope scopes pat =
+  try 
+    if !print_no_symbol then raise No_match;
+    let (sc,n) = Symbols.uninterp_cases_numeral pat in
+    match Symbols.availability_of_numeral sc scopes with
+    | None -> raise No_match
+    | Some scopt -> insert_pat_delimiters (CPatNumeral (loc,n)) scopt
+  with No_match ->
+  match pat with
+  | PatVar (_,Name id) -> CPatAtom (loc,Some (Ident (loc,id)))
+  | PatVar (_,Anonymous) -> CPatAtom (loc, None) 
+  | PatCstr(_,cstrsp,args,na) ->
+      let args = List.map (extern_cases_pattern_in_scope scopes) args in
       let p = CPatCstr (loc,extern_ref (ConstructRef cstrsp),args) in
       (match na with
 	| Name id -> CPatAlias (loc,p,id)
@@ -140,14 +160,31 @@ let rec skip_coercion dest_ref (f,args as app) =
     with Not_found -> app
 
 let extern_app impl f args =
-  if !print_implicits & not !print_implicits_explicit_args then 
+  if (!print_implicits & not !print_implicits_explicit_args) then 
     CAppExpl (dummy_loc, f, args)
   else
     explicitize impl (CRef f) args
 
-let loc = dummy_loc
+let rec extern_args extern scopes args subscopes =
+  match args with
+    | [] -> []
+    | a::args ->
+	let argscopes, subscopes = match subscopes with
+	  | [] -> scopes, []
+	  | scopt::subscopes -> option_cons scopt scopes, subscopes in
+	extern argscopes a :: extern_args extern scopes args subscopes
+
+let rec extern scopes r =
+  try 
+    if !print_no_symbol then raise No_match;
+    extern_numeral scopes r (Symbols.uninterp_numeral r)
+  with No_match ->
+
+  try 
+    if !print_no_symbol then raise No_match;
+    extern_symbol scopes r (Symbols.uninterp_notations r)
+  with No_match -> match r with
 
-let rec extern = function
   | RRef (_,ref) -> CRef (extern_ref ref)
 
   | RVar (_,id) -> CRef (Ident (loc,id))
@@ -159,51 +196,55 @@ let rec extern = function
   | RApp (_,f,args) ->
       let (f,args) =
 	skip_coercion (function RRef(_,r) -> Some r | _ -> None) (f,args) in
-      let args = List.map extern args in
       (match f with
 	 | REvar (loc,ev) -> extern_evar loc ev (* we drop args *)
 	 | RRef (loc,ref) ->
+	     let subscopes = Symbols.find_arguments_scope ref in
+	     let args = extern_args extern scopes args subscopes in
 	     extern_app (implicits_of_global ref) (extern_ref ref) args
-	 | _       -> explicitize [] (extern f) args)
+	 | _       -> 
+	     explicitize [] (extern scopes f) (List.map (extern scopes) args))
 
   | RProd (_,Anonymous,t,c) ->
       (* Anonymous product are never factorized *)
-      CArrow (loc,extern t,extern c)
+      CArrow (loc,extern scopes t,extern scopes c)
 
   | RLetIn (_,na,t,c) ->
-      CLetIn (loc,(loc,na),extern t,extern c)
+      CLetIn (loc,(loc,na),extern scopes t,extern scopes c)
 
   | RProd (_,na,t,c) ->
-      let t = extern t in
-      let (idl,c) = factorize_prod t c in
+      let t = extern scopes t in
+      let (idl,c) = factorize_prod scopes t c in
       CProdN (loc,[(loc,na)::idl,t],c)
 
   | RLambda (_,na,t,c) ->
-      let t = extern t in
-      let (idl,c) = factorize_lambda t c in
+      let t = extern scopes t in
+      let (idl,c) = factorize_lambda scopes t c in
       CLambdaN (loc,[(loc,na)::idl,t],c)
 
   | RCases (_,typopt,tml,eqns) ->
-      let pred = option_app extern typopt in
-      let tml = List.map extern tml in
-      let eqns = List.map extern_eqn eqns in 
+      let pred = option_app (extern scopes) typopt in
+      let tml = List.map (extern scopes) tml in
+      let eqns = List.map (extern_eqn scopes) eqns in 
       CCases (loc,pred,tml,eqns)
 	
   | ROrderedCase (_,cs,typopt,tm,bv) ->
-      let bv = Array.to_list (Array.map extern bv) in
-      COrderedCase (loc,cs,option_app extern typopt,extern tm,bv)
+      let bv = Array.to_list (Array.map (extern scopes) bv) in
+      COrderedCase
+	(loc,cs,option_app (extern scopes) typopt,extern scopes tm,bv)
 
   | RRec (_,fk,idv,tyv,bv) ->
       (match fk with
 	 | RFix (nv,n) ->
 	     let listdecl = 
-	       Array.mapi
-		 (fun i fi -> (fi,nv.(i),extern tyv.(i),extern bv.(i))) idv
+	       Array.mapi (fun i fi ->
+		 (fi,nv.(i),extern scopes tyv.(i),extern scopes bv.(i))) idv
 	     in 
 	     CFix (loc,(loc,idv.(n)),Array.to_list listdecl)
 	 | RCoFix n -> 
 	     let listdecl =
-               Array.mapi (fun i fi -> (fi,extern tyv.(i),extern bv.(i))) idv
+               Array.mapi (fun i fi ->
+		 (fi,extern scopes tyv.(i),extern scopes bv.(i))) idv
 	     in
 	     CCoFix (loc,(loc,idv.(n)),Array.to_list listdecl))
 
@@ -216,46 +257,71 @@ let rec extern = function
 
   | RHole (_,e) -> CHole loc
 
-  | RCast (_,c,t) -> CCast (loc,extern c,extern t)
+  | RCast (_,c,t) -> CCast (loc,extern scopes c,extern scopes t)
 
   | RDynamic (_,d) -> CDynamic (loc,d)
 	
-and factorize_prod aty = function
+and factorize_prod scopes aty = function
   | RProd (_,Name id,ty,c)
-      when aty = extern ty
-	& not (occur_var_constr_expr id aty) (*To avoid na in ty escapes scope*)
-	-> let (nal,c) = factorize_prod aty c in ((loc,Name id)::nal,c)
-  | c -> ([],extern c)
+      when aty = extern scopes ty
+	& not (occur_var_constr_expr id aty) (* avoid na in ty escapes scope *)
+	-> let (nal,c) = factorize_prod scopes aty c in ((loc,Name id)::nal,c)
+  | c -> ([],extern scopes c)
 
-and factorize_lambda aty = function
+and factorize_lambda scopes aty = function
   | RLambda (_,na,ty,c)
-      when aty = extern ty
+      when aty = extern scopes ty
 	& not (occur_name na aty) (* To avoid na in ty' escapes scope *)
-	-> let (nal,c) = factorize_lambda aty c in ((loc,na)::nal,c)
-  | c -> ([],extern c)
-
-and extern_eqn (loc,ids,pl,c) =
-  (loc,List.map extern_cases_pattern pl,extern c)
-(*
-and extern_numerals r =
-  on_numeral (fun p ->
-    match filter p r with
-      | Some f 
-
-and extern_symbols r =
-*)
-
-let extern_rawconstr = extern
+	-> let (nal,c) = factorize_lambda scopes aty c in ((loc,na)::nal,c)
+  | c -> ([],extern scopes c)
+
+and extern_eqn scopes (loc,ids,pl,c) =
+  (loc,List.map (extern_cases_pattern_in_scope scopes) pl,extern scopes c)
+
+and extern_numeral scopes t (sc,n) =
+  match Symbols.availability_of_numeral sc scopes with
+    | None -> raise No_match
+    | Some scopt -> insert_delimiters (CNumeral (loc,n)) scopt
+
+and extern_symbol scopes t = function
+  | [] -> raise No_match
+  | (sc,ntn,pat,n as rule)::rules ->
+      try
+	(* Adjusts to the number of arguments expected by the notation *)
+	let (t,args) = match t,n with
+	  | RApp (_,f,args), Some n when List.length args > n ->
+	      let args1, args2 = list_chop n args in
+	      RApp (loc,f,args1), args2
+	  | _ -> t,[] in
+	(* Try matching ... *)
+	let subst = match_aconstr t pat in
+	(* Try availability of interpretation ... *)
+	(match Symbols.availability_of_notation (sc,ntn) scopes with
+          (* Uninterpretation is not allowed in current context *)
+	  | None -> raise No_match
+          (* Uninterpretation is allowed in current context *)
+	  | Some scopt ->
+	      let scopes = option_cons scopt scopes in
+	      let l = List.map (fun (id,c) -> (id,extern scopes c)) subst in
+	      let e = insert_delimiters (CNotation (loc,ntn,l)) scopt in
+	      if args = [] then e 
+	      else explicitize [] e (List.map (extern scopes) args))
+      with
+	  No_match -> extern_symbol scopes t rules
+
+let extern_rawconstr = 
+  extern (Symbols.current_scopes())
+
+let extern_cases_pattern = 
+  extern_cases_pattern_in_scope (Symbols.current_scopes())
 
 (******************************************************************)
 (* Main translation function from constr -> constr_expr *)
        
 let extern_constr at_top env t =
-  let t' =
-    if !print_casts then t
-    else Reductionops.local_strong strip_outer_cast t in
   let avoid = if at_top then ids_of_context env else [] in
-  extern (Detyping.detype env avoid (names_of_rel_context env) t')
+  extern (Symbols.current_scopes())
+    (Detyping.detype env avoid (names_of_rel_context env) t)
 
 (******************************************************************)
 (* Main translation function from pattern -> constr_expr *)
@@ -319,9 +385,12 @@ let rec extern_pattern tenv env = function
 	(loc,cs,option_app (extern_pattern tenv env) typopt,
 	 extern_pattern tenv env tm,bv)
 
-  | PFix f -> extern (Detyping.detype tenv [] env (mkFix f))
+  | PFix f ->
+      extern (Symbols.current_scopes()) (Detyping.detype tenv [] env (mkFix f))
 
-  | PCoFix c -> extern (Detyping.detype tenv [] env (mkCoFix c))
+  | PCoFix c ->
+      extern (Symbols.current_scopes())
+        (Detyping.detype tenv [] env (mkCoFix c))
 
   | PSort s ->
       let s = match s with
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index cfa00c0068..614cbfdd42 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -19,6 +19,7 @@ open Nametab
 open Rawterm
 open Pattern
 open Topconstr
+open Symbols
 (*i*)
 
 (* Translation of pattern, cases pattern, rawterm and term into syntax
@@ -36,14 +37,23 @@ val extern_ref    : global_reference -> reference
 
 (* For debugging *)
 val print_implicits : bool ref
-val print_casts : bool ref
 val print_arguments : bool ref
 val print_evar_arguments : bool ref
 val print_coercions : bool ref
 val print_universes : bool ref
 
-val with_casts : ('a -> 'b) -> 'a -> 'b
+(* This governs printing of implicit arguments. If [with_implicits] is
+   on and not [with_arguments] then implicit args are printed prefixed
+   by "!"; if [with_implicits] and [with_arguments] are both on the
+   function and not the arguments is prefixed by "!" *)
 val with_implicits : ('a -> 'b) -> 'a -> 'b
 val with_arguments : ('a -> 'b) -> 'a -> 'b
+
+(* This forces printing of coercions *)
 val with_coercions : ('a -> 'b) -> 'a -> 'b
+
+(* This forces printing universe names of Type{.} *)
 val with_universes : ('a -> 'b) -> 'a -> 'b
+
+(* This suppresses printing of numeral and symbols *)
+val without_symbols : ('a -> 'b) -> 'a -> 'b
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index e760f3e929..7236335c39 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -117,23 +117,21 @@ let add_glob loc ref =
    [vars2] is the set of global variables, env is the set of variables
    abstracted until this point *)
 
-(* Is it a bound variables? *)
 let intern_var (env,impls,_) (vars1,vars2) loc id =
+  (* Is [id] bound in  *)
+  if Idset.mem id env or List.mem id vars1
+  then
+    RVar (loc,id), (try List.assoc id impls with Not_found -> []), []
+  else
+  (* Is [id] a section variable *)
+  let _ = Sign.lookup_named id vars2 in
+  (* Car Fixpoint met les fns définies temporairement comme vars de sect *)
   let imps, args_scopes =
-    (* Is [id] bound in  *)
-    if Idset.mem id env or List.mem id vars1
-    then
-      try List.assoc id impls, []
-      with Not_found -> [], []
-    else
-    (* Is [id] a section variable *)
-    let _ = Sign.lookup_named id vars2 in
-    (* Car Fixpoint met les fns définies temporairement comme vars de sect *)
     try
       let ref = VarRef id in
       implicits_of_global ref, find_arguments_scope ref
-    with _ -> [], []
-  in RVar (loc, id), imps, args_scopes
+    with _ -> [], [] in
+  RRef (loc, VarRef id), imps, args_scopes
 
 (* Is it a global reference or a syntactic definition? *)
 let intern_qualid env vars loc qid =
@@ -334,11 +332,8 @@ let coerce_to_id = function
         str"This expression should be a simple identifier")
 
 let traverse_binder id (subst,(ids,impls,scopes as env)) =
-  try 
-    let id' = coerce_to_id (List.assoc id subst) in
-    id', (subst,(Idset.add id' ids,impls,scopes))
-  with Not_found ->
-    id, (List.remove_assoc id subst,env)
+  let id = try coerce_to_id (List.assoc id subst) with Not_found -> id in
+  id,(subst,(Idset.add id ids,impls,scopes))
 
 let rec subst_rawconstr loc interp (subst,env as senv) = function
   | AVar id ->
diff --git a/interp/symbols.ml b/interp/symbols.ml
index c6eff9ab96..87282f0467 100644
--- a/interp/symbols.ml
+++ b/interp/symbols.ml
@@ -14,6 +14,7 @@ open Pp
 open Bignat
 open Names
 open Nametab
+open Libnames
 open Summary
 open Rawterm
 open Topconstr
@@ -41,7 +42,7 @@ open Ppextend
 type level = precedence * precedence list
 type delimiters = string * string
 type scope = {
-  notations: (aconstr * level) Stringmap.t;
+  notations: (aconstr * (level * string)) Stringmap.t;
   delimiters: delimiters option
 }
 type scopes = scope_name list
@@ -58,6 +59,9 @@ let default_scope = "core_scope"
 
 let _ = Stringmap.add default_scope empty_scope !scope_map
 
+(**********************************************************************)
+(* The global stack of scopes                                         *)
+
 let scope_stack = ref [default_scope]
 
 let current_scopes () = !scope_stack
@@ -65,26 +69,8 @@ let current_scopes () = !scope_stack
 (* TODO: push nat_scope, z_scope, ... in scopes summary *)
 
 (**********************************************************************)
-(* Interpreting numbers (not in summary because functional objects)   *)
-
-type numeral_interpreter_name = string
-type numeral_interpreter =
-    (loc -> bigint -> rawconstr)
-    * (loc -> bigint -> name -> cases_pattern) option
-
-let numeral_interpreter_tab =
-  (Hashtbl.create 17 : (numeral_interpreter_name,numeral_interpreter)Hashtbl.t)
-
-let declare_numeral_interpreter sc t =
-  Hashtbl.add numeral_interpreter_tab sc t
-
-let lookup_numeral_interpreter s =
-  try 
-    Hashtbl.find numeral_interpreter_tab s
-  with Not_found -> 
-    error ("No interpretation for numerals in scope "^s)
+(* Operations on scopes *)
 
-(* For loading without opening *)
 let declare_scope scope =
   try let _ = Stringmap.find scope !scope_map in ()
   with Not_found ->
@@ -97,6 +83,9 @@ let find_scope scope =
 
 let check_scope sc = let _ = find_scope sc in ()
 
+(**********************************************************************)
+(* Delimiters *)
+
 let declare_delimiters scope dlm =
   let sc = find_scope scope in
   if sc.delimiters <> None && Options.is_verbose () then
@@ -104,105 +93,147 @@ let declare_delimiters scope dlm =
   let sc = { sc with delimiters = Some dlm } in
   scope_map := Stringmap.add scope sc !scope_map   
 
-(* The mapping between notations and production *)
+let find_delimiters scope = (find_scope scope).delimiters
 
-let declare_notation nt scope (c,prec as info) =
-  let sc = find_scope scope in
-  if Stringmap.mem nt sc.notations && Options.is_verbose () then
-    warning ("Notation "^nt^" is already used in scope "^scope);
-  let sc = { sc with notations = Stringmap.add nt info sc.notations } in
-  scope_map := Stringmap.add scope sc !scope_map
+(* Uninterpretation tables *)
 
-let rec find_interpretation f = function
-  | scope::scopes ->
-      (try f (find_scope scope)
-       with Not_found -> find_interpretation f scopes)
-  | [] -> raise Not_found
+type interpretation = identifier list * aconstr
+type interp_rule = scope_name * notation * interpretation * int option
 
-let rec interp_notation ntn scopes =
-  let f scope = fst (Stringmap.find ntn scope.notations) in
-  try find_interpretation f scopes
-  with Not_found -> anomaly ("Unknown interpretation for notation "^ntn)
+(* We define keys for rawterm and aconstr to split the syntax entries
+   according to the key of the pattern (adapted from Chet Murthy by HH) *)
 
-let find_notation_with_delimiters scope =
-  match (Stringmap.find scope !scope_map).delimiters with
-    | Some dlm -> Some (Some dlm)
-    | None -> None
+type key =
+  | RefKey of global_reference
+  | Oth
 
-let rec find_notation_without_delimiters ntn_scope ntn = function
-  | scope::scopes ->
-      (* Is the expected printer attached to the most recently open scope? *)
-      if scope = ntn_scope then
-	Some None
-      else
-	(* If the most recently open scope has a printer for this pattern
-    	   but not the expected one then we need delimiters *)
-	if Stringmap.mem ntn (Stringmap.find scope !scope_map).notations then
-	  find_notation_with_delimiters ntn_scope
-	else
-	  find_notation_without_delimiters ntn_scope ntn scopes
-  | [] ->
-      find_notation_with_delimiters ntn_scope
+(* Scopes table : interpretation -> scope_name *)
+let notations_key_table = ref Gmapl.empty
+let numeral_key_table = Hashtbl.create 7
 
-let find_notation ntn_scope ntn scopes =
-  match 
-    find_notation_without_delimiters ntn_scope ntn scopes
-  with
-    | None -> None
-    | Some None -> Some (None,scopes)
-    | Some x -> Some (x,ntn_scope::scopes)
+let rawconstr_key = function
+  | RApp (_,RRef (_,ref),_) -> RefKey ref
+  | RRef (_,ref) -> RefKey ref
+  | _ -> Oth
 
-let exists_notation_in_scope scope prec ntn r =
-  try Stringmap.find ntn (Stringmap.find scope !scope_map).notations = (r,prec)
-  with Not_found -> false
+let aconstr_key = function
+  | AApp (ARef ref,args) -> RefKey ref, Some (List.length args)
+  | ARef ref -> RefKey ref, Some 0
+  | _ -> Oth, None
 
-let exists_notation_prec prec nt sc =
-  try snd (Stringmap.find nt sc.notations) = prec with Not_found -> false
+let pattern_key = function
+  | PatCstr (_,cstr,_,_) -> RefKey (ConstructRef cstr)
+  | _ -> Oth
 
-let exists_notation prec nt =
-  Stringmap.fold (fun scn sc b -> b or exists_notation_prec prec nt sc)
-    !scope_map false 
+(**********************************************************************)
+(* Interpreting numbers (not in summary because functional objects)   *)
 
-(* We have to print delimiters; look for the more recent defined one *)
-(* Do we need to print delimiters? To know it, we look for a numeral *)
-(* printer available in the current stack of scopes *)
-let find_numeral_with_delimiters scope =
+type num_interpreter =
+    (loc -> bigint -> rawconstr)
+    * (loc -> bigint -> name -> cases_pattern) option
+
+type num_uninterpreter =
+    rawconstr list * (rawconstr -> bigint option)
+    * (cases_pattern -> bigint option) option
+
+type required_module = string list 
+
+let numeral_interpreter_tab =
+  (Hashtbl.create 7 : (scope_name,required_module*num_interpreter) Hashtbl.t)
+
+let declare_numeral_interpreter sc dir interp (patl,uninterp,uninterpc) =
+  declare_scope sc;
+  Hashtbl.add numeral_interpreter_tab sc (dir,interp);
+  List.iter
+    (fun pat -> Hashtbl.add numeral_key_table (rawconstr_key pat)
+      (sc,uninterp,uninterpc))
+    patl
+
+let check_required_module loc sc d =
+  let d' = List.map id_of_string d in
+  let dir = make_dirpath (List.rev d') in
+  if not (Library.library_is_loaded dir) then
+    user_err_loc (loc,"numeral_interpreter",
+    str ("Cannot interpret numbers in "^sc^" without requiring first module "
+    ^(list_last d)))
+
+let lookup_numeral_interpreter loc sc =
+  try
+    let (dir,interpreter) = Hashtbl.find numeral_interpreter_tab sc in
+    check_required_module loc sc dir;
+    interpreter
+  with Not_found -> 
+    error ("No interpretation for numerals in scope "^sc)
+
+(* Look if some notation or numeral printer in [scope] can be used in
+   the scope stack [scopes], and if yes, using delimiters or not *)
+
+let find_with_delimiters scope =
   match (Stringmap.find scope !scope_map).delimiters with
-    | Some dlm -> Some (Some dlm)
+    | Some _ -> Some (Some scope)
     | None -> None
 
-let rec find_numeral_without_delimiters printer_scope = function
+let rec find_without_delimiters find ntn_scope = function
   | scope :: scopes -> 
-      (* Is the expected printer attached to the most recently open scope? *)
-      if scope = printer_scope then
+      (* Is the expected ntn/numpr attached to the most recently open scope? *)
+      if scope = ntn_scope then
 	Some None
       else
-	(* If the most recently open scope has a printer for numerals
+	(* If the most recently open scope has a notation/numeral printer
     	   but not the expected one then we need delimiters *)
-	if not (Hashtbl.mem numeral_interpreter_tab scope) then
-	  find_numeral_without_delimiters printer_scope scopes
+	if find scope then
+	  find_with_delimiters ntn_scope
 	else
-	  find_numeral_with_delimiters printer_scope
+	  find_without_delimiters find ntn_scope scopes
   | [] ->
       (* Can we switch to [scope]? Yes if it has defined delimiters *)
-      find_numeral_with_delimiters printer_scope
+      find_with_delimiters ntn_scope
+
+(* The mapping between notations and their interpretation *)
+
+let declare_interpretation ntn scope pat =
+  let sc = find_scope scope in
+  if Stringmap.mem ntn sc.notations && Options.is_verbose () then
+    warning ("Notation "^ntn^" is already used in scope "^scope);
+  let sc = { sc with notations = Stringmap.add ntn pat sc.notations } in
+  scope_map := Stringmap.add scope sc !scope_map
+
+let declare_uninterpretation ntn scope metas c =
+  let (key,n) = aconstr_key c in
+  notations_key_table :=
+    Gmapl.add key (scope,ntn,(metas,c),n) !notations_key_table
 
-let find_numeral_printer printer_scope scopes =
+let declare_notation ntn scope (metas,c) prec df onlyparse =
+  declare_interpretation ntn scope (c,(prec,df));
+  if not onlyparse then declare_uninterpretation ntn scope metas c
+
+let rec find_interpretation f = function
+  | scope::scopes ->
+      (try f (find_scope scope)
+       with Not_found -> find_interpretation f scopes)
+  | [] -> raise Not_found
+
+let rec interp_notation ntn scopes =
+  let f scope = fst (Stringmap.find ntn scope.notations) in
+  try find_interpretation f scopes
+  with Not_found -> anomaly ("Unknown interpretation for notation "^ntn)
+
+let uninterp_notations c =
+  Gmapl.find (rawconstr_key c) !notations_key_table
+
+let availability_of_notation (ntn_scope,ntn) scopes =
   match 
-    find_numeral_without_delimiters printer_scope scopes
+    let f scope =
+      Stringmap.mem ntn (Stringmap.find scope !scope_map).notations in
+    find_without_delimiters f ntn_scope scopes
   with
     | None -> None
-    | Some None -> Some (None,scopes)
-    | Some x -> Some (x,printer_scope::scopes)
-
-(* This is the map associating the scope a numeral printer belongs to *)
-(*
-let numeral_printer_map = ref (Stringmap.empty : scope_name Stringmap.t)
-*)
+    | Some None -> Some None
+    | Some (Some dlm) -> Some (Some ntn_scope)
 
 let rec interp_numeral loc n = function
   | scope :: scopes ->
-      (try fst (lookup_numeral_interpreter scope) loc n
+      (try fst (lookup_numeral_interpreter loc scope) loc n
        with Not_found -> interp_numeral loc n scopes)
   | [] ->
       user_err_loc (loc,"interp_numeral",
@@ -211,7 +242,7 @@ let rec interp_numeral loc n = function
 let rec interp_numeral_as_pattern loc n name = function
   | scope :: scopes ->
       (try 
-	match snd (lookup_numeral_interpreter scope) with
+	match snd (lookup_numeral_interpreter loc scope) with
 	  | None -> raise Not_found
 	  | Some g -> g loc n name
 	with Not_found -> interp_numeral_as_pattern loc n name scopes)
@@ -219,6 +250,48 @@ let rec interp_numeral_as_pattern loc n name = function
       user_err_loc (loc,"interp_numeral_as_pattern",
       str "No interpretation for numeral " ++ pr_bigint n)
 
+let uninterp_numeral c =
+  try 
+    let (sc,numpr,_) = Hashtbl.find numeral_key_table (rawconstr_key c) in
+    match numpr c with
+      | None -> raise No_match
+      | Some n -> (sc,n)
+  with Not_found -> raise No_match
+
+let uninterp_cases_numeral c =
+  try 
+    match Hashtbl.find numeral_key_table (pattern_key c) with
+      | (_,_,None) -> raise No_match
+      | (sc,_,Some numpr) ->
+	  match numpr c with
+	    | None -> raise No_match
+	    | Some n -> (sc,n)
+  with Not_found -> raise No_match
+
+let availability_of_numeral printer_scope scopes =
+  match 
+    let f scope = Hashtbl.mem numeral_interpreter_tab scope in
+    find_without_delimiters f printer_scope scopes
+  with
+    | None -> None
+    | Some x -> Some x
+
+(* Miscellaneous *)
+
+let exists_notation_in_scope scope prec ntn r =
+  try
+    let sc = Stringmap.find scope !scope_map in
+    let (r',(prec',_)) = Stringmap.find ntn sc.notations in
+    r' = r & prec = prec'
+  with Not_found -> false
+
+let exists_notation_prec prec nt sc =
+  try fst (snd (Stringmap.find nt sc.notations)) = prec with Not_found -> false
+
+let exists_notation prec nt =
+  Stringmap.fold (fun scn sc b -> b or exists_notation_prec prec nt sc)
+    !scope_map false 
+
 (* Exportation of scopes *)
 let cache_scope (_,sc) =
   check_scope sc;
@@ -238,19 +311,8 @@ let (inScope,outScope) =
 
 let open_scope sc = Lib.add_anonymous_leaf (inScope sc)
 
-
 (* Special scopes associated to arguments of a global reference *)
 
-open Libnames
-
-module RefOrdered =
-  struct
-    type t = global_reference
-    let compare = Pervasives.compare
-  end
-
-module Refmap = Map.Make(RefOrdered)
-
 let arguments_scope = ref Refmap.empty
 
 let cache_arguments_scope (_,(r,scl)) =
@@ -276,18 +338,22 @@ let find_arguments_scope r =
 
 (* Printing *)
 
-let pr_delimiters = function
+let pr_delimiters_info = function
   | None -> str "No delimiters"
   | Some (l,r) -> str "Delimiters are " ++ str l ++ str " and " ++ str r
 
-let pr_notation prraw ntn r =
-  str ntn ++ str " stands for " ++ prraw r
+let rec rawconstr_of_aconstr () x =
+  map_aconstr_with_binders_loc dummy_loc (fun id () -> (id,())) 
+    rawconstr_of_aconstr () x
+
+let pr_notation_info prraw ntn c =
+  str ntn ++ str " stands for " ++ prraw (rawconstr_of_aconstr () c)
 
 let pr_named_scope prraw scope sc =
   str "Scope " ++ str scope ++ fnl ()
-  ++ pr_delimiters sc.delimiters ++ fnl ()
+  ++ pr_delimiters_info sc.delimiters ++ fnl ()
   ++ Stringmap.fold
-       (fun ntn (r,_) strm -> pr_notation prraw ntn r ++ fnl () ++ strm)
+       (fun ntn (r,(_,df)) strm -> pr_notation_info prraw df r ++ fnl () ++ strm)
        sc.notations (mt ())
 
 let pr_scope prraw scope = pr_named_scope prraw scope (find_scope scope)
@@ -297,20 +363,44 @@ let pr_scopes prraw =
    (fun scope sc strm -> pr_named_scope prraw scope sc ++ fnl () ++ strm)
    !scope_map (mt ())
 
+(**********************************************************************)
+(* Mapping notations to concrete syntax *)
+
+type unparsing_rule = unparsing list * precedence
+
+(* Concrete syntax for symbolic-extension table *)
+let printing_rules = 
+  ref (Stringmap.empty : unparsing_rule Stringmap.t)
+
+let declare_notation_printing_rule ntn unpl =
+  printing_rules := Stringmap.add ntn unpl !printing_rules
+
+let find_notation_printing_rule ntn =
+  try Stringmap.find ntn !printing_rules
+  with Not_found -> anomaly ("No printing rule found for "^ntn)
+
+(**********************************************************************)
 (* Synchronisation with reset *)
 
-let freeze () = (!scope_map, !scope_stack, !arguments_scope)
+let freeze () =
+ (!scope_map, !scope_stack, !arguments_scope,
+  !notations_key_table, !printing_rules)
 
-let unfreeze (scm,scs,asc) =
+let unfreeze (scm,scs,asc,fkm,pprules) =
   scope_map := scm;
   scope_stack := scs;
-  arguments_scope := asc
+  arguments_scope := asc;
+  notations_key_table := fkm;
+  printing_rules := pprules
 
-let init () = ()
+let init () =
 (*
   scope_map := Strinmap.empty;
   scope_stack := Stringmap.empty
+  arguments_scope := Refmap.empty
 *)
+  notations_key_table := Gmapl.empty;
+  printing_rules := Stringmap.empty
 
 let _ = 
   declare_summary "symbols"
@@ -318,14 +408,3 @@ let _ =
       unfreeze_function = unfreeze;
       init_function = init;
       survive_section = false }
-
-
-let printing_rules = 
-  ref (Stringmap.empty : (unparsing list * precedence) Stringmap.t)
-
-let declare_printing_rule ntn unpl =
-  printing_rules := Stringmap.add ntn unpl !printing_rules
-
-let find_notation_printing_rule ntn =
-  try Stringmap.find ntn !printing_rules
-  with Not_found -> anomaly ("No printing rule found for "^ntn)
diff --git a/interp/symbols.mli b/interp/symbols.mli
index 3c082b2ceb..466a2bb281 100644
--- a/interp/symbols.mli
+++ b/interp/symbols.mli
@@ -14,22 +14,17 @@ open Pp
 open Bignat
 open Names
 open Nametab
+open Libnames
 open Rawterm
 open Topconstr
 open Ppextend
-(*i*)
 
-(*s 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 *)
+(*i*)
 
-type numeral_interpreter_name = string
-type numeral_interpreter =
-    (loc -> bigint -> rawconstr)
-    * (loc -> bigint -> name -> cases_pattern) option
+(**********************************************************************)
+(* Scopes *)
 
-(* A scope is a set of interpreters for symbols + optional
+(*s A scope is a set of interpreters for symbols + optional
    interpreter and printers for integers + optional delimiters *)
 
 type level = precedence * precedence list
@@ -38,40 +33,92 @@ type scope
 type scopes = scope_name list
 
 val default_scope : scope_name
+val declare_scope : scope_name -> unit
+
+(* Open scope *)
+
 val current_scopes : unit -> scopes
 val open_scope : scope_name -> unit
-val declare_scope : scope_name -> unit
 
 (* Declare delimiters for printing *)
+
 val declare_delimiters : scope_name -> delimiters -> unit
+val find_delimiters : scope_name -> delimiters option
+
+(*s Declare and uses back and forth a numeral interpretation *)
+
+(* 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 *)
+
+type num_interpreter =
+    (loc -> bigint -> rawconstr)
+    * (loc -> bigint -> name -> cases_pattern) option
+
+type num_uninterpreter =
+    rawconstr list * (rawconstr -> bigint option)
+    * (cases_pattern -> bigint option) option
 
-(* Declare, interpret, and look for a printer for numeral *)
-val declare_numeral_interpreter :
-  numeral_interpreter_name -> numeral_interpreter -> unit
+type required_module = 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*)
 val interp_numeral : loc -> bigint -> scopes -> rawconstr
 val interp_numeral_as_pattern : loc -> bigint -> name -> scopes ->cases_pattern
-val find_numeral_printer : string -> scopes ->
-  (delimiters option * scopes) option
 
-(* Declare, interpret, and look for a printer for symbolic notations *)
-val declare_notation : notation -> scope_name -> aconstr * level -> unit
+(* Returns the numeral bound to a term/cases_pattern; raises No_match if no *)
+(* such numeral *)
+val uninterp_numeral : rawconstr -> scope_name * bigint
+val uninterp_cases_numeral : cases_pattern -> scope_name * bigint
+
+val availability_of_numeral : scope_name -> scopes -> scope_name option option
+
+(*s Declare and interpret back and forth a notation *)
+
+type interpretation = identifier list * aconstr
+
+(* Binds a notation in a given scope to an interpretation *)
+type interp_rule = scope_name * notation * interpretation * int option
+val declare_notation : notation -> scope_name -> interpretation -> level ->
+  string -> bool -> unit
+
+(* Returns the interpretation bound to a notation *)
 val interp_notation : notation -> scopes -> aconstr
-val find_notation : scope_name -> notation -> scopes -> 
-  (delimiters option * scopes) option
-val exists_notation_in_scope : 
-  scope_name -> level -> notation -> aconstr -> bool
+
+(* Returns the possible notations for a given term *)
+val uninterp_notations : rawconstr -> interp_rule list
+
+(* Test if a notation is available in the scopes *)
+(* context [scopes] if available, the result is not None; the first *)
+(* argument is itself not None if a delimiters is needed; the second *)
+(* argument is a numeral printer if the *)
+val availability_of_notation : scope_name * notation -> scopes -> 
+  scope_name option option
+
+(*s** Miscellaneous *)
+
+(* Checks for already existing notations *)
+val exists_notation_in_scope : scope_name -> level -> notation -> aconstr->bool
 val exists_notation : level -> notation -> bool
 
-(* Declare and look for scopes associated to arguments of a global ref *)
-open Libnames
+(* Declares and looks for scopes associated to arguments of a global ref *)
 val declare_arguments_scope: global_reference -> scope_name option list -> unit
 val find_arguments_scope : global_reference -> scope_name option list
 
-(* Printing scopes *)
-val pr_scope : (aconstr -> std_ppcmds) -> scope_name -> std_ppcmds
-val pr_scopes : (aconstr -> std_ppcmds) -> std_ppcmds
+(* Prints scopes (expect a pure aconstr printer *)
+val pr_scope : (rawconstr -> std_ppcmds) -> scope_name -> std_ppcmds
+val pr_scopes : (rawconstr -> std_ppcmds) -> std_ppcmds
+
+(**********************************************************************)
+(*s Printing rules for notations *)
 
+(* Declare and look for the printing rule for symbolic notations *)
+type unparsing_rule = unparsing list * precedence
+val declare_notation_printing_rule : notation -> unparsing_rule -> unit
+val find_notation_printing_rule : notation -> unparsing_rule
 
-val declare_printing_rule : notation -> unparsing list * precedence -> unit
-val find_notation_printing_rule : notation -> unparsing list * precedence
+(**********************************************************************)
+(* Rem: printing rules for numerals are trivial *)
 
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 8d16602b5c..8173d3fc45 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -18,8 +18,9 @@ open Rawterm
 open Term
 (*i*)
 
-
+(**********************************************************************)
 (* This is the subtype of rawconstr allowed in syntactic extensions *)
+
 type aconstr =
   | ARef of global_reference
   | AVar of identifier
@@ -29,7 +30,7 @@ type aconstr =
   | ALetIn of name * aconstr * aconstr
   | ACases of aconstr option * aconstr list *
       (identifier list * cases_pattern list * aconstr) list
-  | AOldCase of case_style * aconstr option * aconstr * aconstr array
+  | AOrderedCase of case_style * aconstr option * aconstr * aconstr array
   | ASort of rawsort
   | AHole of hole_kind
   | AMeta of int
@@ -53,7 +54,7 @@ let map_aconstr_with_binders_loc loc g f e = function
       let eqnl = List.map (fun (idl,pat,rhs) ->
         let (idl,e) = List.fold_right fold idl ([],e) in (loc,idl,pat,f e rhs)) eqnl in
       RCases (loc,option_app (f e) tyopt,List.map (f e) tml,eqnl)
-  | AOldCase (b,tyopt,tm,bv) ->
+  | AOrderedCase (b,tyopt,tm,bv) ->
       ROrderedCase (loc,b,option_app (f e) tyopt,f e tm,Array.map (f e) bv)
   | ACast (c,t) -> RCast (loc,f e c,f e t)
   | ASort x -> RSort (loc,x)
@@ -114,12 +115,12 @@ let rec subst_aconstr subst raw =
         if ro' == ro && rl' == rl && branches' == branches then raw else
           ACases (ro',rl',branches')
 
-  | AOldCase (b,ro,r,ra) -> 
+  | AOrderedCase (b,ro,r,ra) -> 
       let ro' = option_smartmap (subst_aconstr subst) ro
       and r' = subst_aconstr subst r 
       and ra' = array_smartmap (subst_aconstr subst) ra in
 	if ro' == ro && r' == r && ra' == ra then raw else
-	  AOldCase (b,ro',r',ra')
+	  AOrderedCase (b,ro',r',ra')
 
   | AMeta _ | ASort _ -> raw
 
@@ -145,7 +146,7 @@ let rec aux = function
       let eqnl = List.map (fun (_,idl,pat,rhs) -> (idl,pat,aux rhs)) eqnl in
       ACases (option_app aux tyopt,List.map aux tml, eqnl)
   | ROrderedCase (_,b,tyopt,tm,bv) ->
-      AOldCase (b,option_app aux tyopt,aux tm, Array.map aux bv)
+      AOrderedCase (b,option_app aux tyopt,aux tm, Array.map aux bv)
   | RCast (_,c,t) -> ACast (aux c,aux t)
   | RSort (_,s) -> ASort s
   | RHole (_,w) -> AHole w
@@ -157,6 +158,75 @@ allowed in abbreviatable expressions"
 
 let aconstr_of_rawconstr = aux
 
+(* Pattern-matching rawconstr and aconstr *)
+
+exception No_match
+
+let rec alpha_var id1 id2 = function
+  | (i1,i2)::_ when i1=id1 -> i2 = id2
+  | (i1,i2)::_ when i2=id2 -> i1 = id1
+  | _::idl -> alpha_var id1 id2 idl
+  | [] -> id1 = id2
+
+let alpha_eq_val (x,y) = x = y
+
+let bind_env 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 -> 
+    (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
+  | RVar (_,id1), AVar id2 when alpha_var id1 id2 alp -> sigma
+  | RRef (_,r1), ARef r2 when r1 = r2 -> sigma
+  | RMeta (_,n1), AMeta n2 when n1=n2 -> sigma
+  | RApp (_,f1,l1), AApp (f2,l2) when List.length l1 = List.length l2 ->
+      List.fold_left2 (match_ alp metas) (match_ alp metas sigma f1 f2) l1 l2
+  | RLambda (_,na1,t1,b1), ALambda (na2,t2,b2) ->
+     match_binders alp metas (match_ alp metas sigma t1 t2) b1 b2 na1 na2
+  | RProd (_,na1,t1,b1), AProd (na2,t2,b2) ->
+     match_binders alp metas (match_ alp metas sigma t1 t2) b1 b2 na1 na2
+  | RLetIn (_,na1,t1,b1), AProd (na2,t2,b2) ->
+     match_binders alp metas (match_ alp metas sigma t1 t2) b1 b2 na1 na2
+  | RCases (_,po1,tml1,eqnl1), ACases (po2,tml2,eqnl2) ->
+     let sigma = option_fold_left2 (match_ alp metas) sigma po1 po2 in
+     let sigma = List.fold_left2 (match_ alp metas) sigma tml1 tml2 in
+     List.fold_left2 (match_equations alp metas) sigma eqnl1 eqnl2
+  | ROrderedCase (_,st,po1,c1,bl1), AOrderedCase (st2,po2,c2,bl2) ->
+     let sigma = option_fold_left2 (match_ alp metas) sigma po1 po2 in
+     array_fold_left2 (match_ alp metas) (match_ alp metas sigma c1 c2) bl1 bl2
+  | RCast(_,c1,t1), ACast(c2,t2) ->
+      match_ alp metas (match_ alp metas sigma c1 c2) t1 t2
+  | RSort (_,s1), ASort s2 when s1 = s2 -> sigma
+  | RHole _, a -> sigma
+  | a, AHole _ -> sigma
+  | (RDynamic _ | RRec _ | REvar _), _ 
+  | _,_ -> raise No_match
+
+and match_binders alp metas sigma b1 b2 na1 na2 = match (na1,na2) with
+  | (na1,Name id2) when List.mem id2 metas ->
+      let sigma =
+	name_fold
+	  (fun id sigma -> bind_env sigma id2 (RVar (dummy_loc,id))) na1 sigma
+      in 
+      match_ alp metas sigma b1 b2
+  | (na1,na2) -> 
+      let alp =
+        name_fold
+	  (fun id1 -> name_fold (fun id2 alp -> (id1,id2)::alp) na2) na1 alp in
+      match_ alp metas sigma b1 b2
+
+and match_equations alp metas sigma (_,idl1,pat1,rhs1) (idl2,pat2,rhs2) =
+  if idl1 = idl2 & pat1 = pat2 (* Useful to reason up to alpha ?? *) then
+    match_ alp metas sigma rhs1 rhs2
+  else raise No_match
+
+let match_aconstr c (metas,pat) = match_ [] metas [] c pat
+
+(**********************************************************************)
 (*s Concrete syntax for terms *)
 
 type scope_name = string
@@ -200,6 +270,16 @@ and fixpoint_expr = identifier * int * constr_expr * constr_expr
 
 and cofixpoint_expr = identifier * constr_expr * constr_expr
 
+(***********************)
+(* For binders parsing *)
+
+type local_binder =
+  | LocalRawDef of name located * constr_expr
+  | LocalRawAssum of name located list * constr_expr
+
+(**********************************************************************)
+(* Functions on constr_expr *)
+
 let constr_loc = function
   | CRef (Ident (loc,_)) -> loc
   | CRef (Qualid (loc,_)) -> loc
@@ -230,9 +310,6 @@ let cases_pattern_loc = function
   | CPatNumeral (loc,_) -> loc
   | CPatDelimiters (loc,_,_) -> loc
 
-let replace_vars_constr_expr l t =
-  if l = [] then t else failwith "replace_constr_expr: TODO"
-
 let occur_var_constr_ref id = function
   | Ident (loc,id') -> id = id'
   | Qualid _ -> false
@@ -307,12 +384,14 @@ let map_constr_expr_with_binders f g e = function
   | CCoFix (loc,id,dl) ->
       CCoFix (loc,id,List.map (fun (id,t,d) -> (id,f e t,f e d)) dl)
 
-(* For binders parsing *)
-
-type local_binder =
-  | LocalRawDef of name located * constr_expr
-  | LocalRawAssum of name located list * constr_expr
+(* Used in constrintern *)
+let rec replace_vars_constr_expr l = function
+  | CRef (Ident (loc,id)) as x ->
+      (try CRef (Ident (loc,List.assoc id l)) with Not_found -> x)
+  | c -> map_constr_expr_with_binders replace_vars_constr_expr 
+      (fun id l -> List.remove_assoc id l) l c
 
+(**********************************************************************)
 (* Concrete syntax for modules and modules types *)
 
 type with_declaration_ast = 
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 2c276ca991..85b05a4faa 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -31,7 +31,7 @@ type aconstr =
   | ALetIn of name * aconstr * aconstr
   | ACases of aconstr option * aconstr list *
       (identifier list * cases_pattern list * aconstr) list
-  | AOldCase of case_style * aconstr option * aconstr * aconstr array
+  | AOrderedCase of case_style * aconstr option * aconstr * aconstr array
   | ASort of rawsort
   | AHole of hole_kind
   | AMeta of int
@@ -45,6 +45,12 @@ val subst_aconstr : Names.substitution -> aconstr -> aconstr
 
 val aconstr_of_rawconstr : rawconstr -> aconstr
 
+(* [match_aconstr metas] match a rawconstr against an aconstr with
+   metavariables in [metas]; it raises [No_match] if the matching fails *)
+exception No_match
+val match_aconstr : 
+  rawconstr -> (identifier list * aconstr) -> (identifier * rawconstr) list
+
 (*s Concrete syntax for terms *)
 
 type scope_name = string