New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr

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

14 files changed, 29 insertions, 23 deletions

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index b3b9efcefd..5932765890 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -24,7 +24,7 @@ open Typeclasses
 open Libnames
 open Constrintern
 open Glob_term
-open Topconstr
+open Constrexpr
 (*i*)
 
 open Decl_kinds
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 424645fe88..4ac722eb20 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -14,7 +14,7 @@ open Evd
 open Environ
 open Nametab
 open Mod_subst
-open Topconstr
+open Constrexpr
 open Errors
 open Util
 open Typeclasses
diff --git a/toplevel/command.ml b/toplevel/command.ml
index ecc4e69953..a1d6eecf2c 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -19,6 +19,7 @@ open Declare
 open Names
 open Libnames
 open Nameops
+open Constrexpr
 open Topconstr
 open Constrintern
 open Nametab
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 3cced65f17..005a4a33af 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -13,7 +13,7 @@ open Entries
 open Libnames
 open Tacexpr
 open Vernacexpr
-open Topconstr
+open Constrexpr
 open Decl_kinds
 open Redexpr
 open Constrintern
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index 00592848fa..78aa3fd12b 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -29,7 +29,7 @@ open Namegen
 open Evd
 open Evarutil
 open Reductionops
-open Topconstr
+open Constrexpr
 open Constrintern
 open Impargs
 open Tacticals
diff --git a/toplevel/lemmas.mli b/toplevel/lemmas.mli
index 35d6aaa268..1c14650464 100644
--- a/toplevel/lemmas.mli
+++ b/toplevel/lemmas.mli
@@ -9,7 +9,7 @@
 open Names
 open Term
 open Decl_kinds
-open Topconstr
+open Constrexpr
 open Tacexpr
 open Vernacexpr
 open Proof_type
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 54de06c9c8..5a305ccc9a 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -12,6 +12,8 @@ open Compat
 open Errors
 open Util
 open Names
+open Constrexpr
+open Notation_term
 open Topconstr
 open Ppextend
 open Extend
@@ -842,7 +844,7 @@ let check_rule_productivity l =
     error "A recursive notation must start with at least one symbol."
 
 let is_not_printable = function
-  | AVar _ -> warning "This notation will not be used for printing as it is bound to a \nsingle variable"; true
+  | NVar _ -> warning "This notation will not be used for printing as it is bound to a \nsingle variable"; true
   | _ -> false
 
 let find_precedence lev etyps symbols =
@@ -1065,7 +1067,7 @@ let add_notation_in_scope local df c mods scope =
   (* Prepare the interpretation *)
   let (onlyparse,recvars,mainvars,df') = i_data in
   let i_vars = make_internalization_vars recvars mainvars i_typs in
-  let (acvars,ac) = interp_aconstr i_vars recvars c in
+  let (acvars,ac) = interp_notation_constr i_vars recvars c in
   let a = (make_interpretation_vars recvars acvars,ac) in
   let onlyparse = onlyparse or is_not_printable ac in
   (* Ready to change the global state *)
@@ -1086,7 +1088,7 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env)
   let path = (Lib.library_dp(),Lib.current_dirpath true) in
   let df' = (make_notation_key symbs,(path,df)) in
   let i_vars = make_internalization_vars recvars mainvars i_typs in
-  let (acvars,ac) = interp_aconstr ~impls i_vars recvars c in
+  let (acvars,ac) = interp_notation_constr ~impls i_vars recvars c in
   let a = (make_interpretation_vars recvars acvars,ac) in
   let onlyparse = onlyparse or is_not_printable ac in
   Lib.add_anonymous_leaf (inNotation (local,scope,a,onlyparse,df'));
@@ -1191,10 +1193,10 @@ let try_interp_name_alias = function
 
 let add_syntactic_definition ident (vars,c) local onlyparse =
   let vars,pat =
-    try [], ARef (try_interp_name_alias (vars,c))
+    try [], NRef (try_interp_name_alias (vars,c))
     with Not_found ->
       let i_vars = List.map (fun id -> (id,NtnInternTypeConstr)) vars in
-      let vars,pat = interp_aconstr i_vars [] c in
+      let vars,pat = interp_notation_constr i_vars [] c in
       List.map (fun (id,(sc,kind)) -> (id,sc)) vars, pat
   in
   let onlyparse = onlyparse or is_not_printable pat in
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index e2a3e33a2f..b7651edec7 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -15,7 +15,8 @@ open Extend
 open Tacexpr
 open Vernacexpr
 open Notation
-open Topconstr
+open Constrexpr
+open Notation_term
 
 val add_token_obj : string -> unit
 
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index c6bb2c10ab..4b26a979d2 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -330,10 +330,10 @@ type obligation =
 type obligations = (obligation array * int)
 
 type fixpoint_kind =
-  | IsFixpoint of (identifier located option * Topconstr.recursion_order_expr) list
+  | IsFixpoint of (identifier located option * Constrexpr.recursion_order_expr) list
   | IsCoFixpoint
 
-type notations = (Vernacexpr.lstring * Topconstr.constr_expr * Topconstr.scope_name option) list
+type notations = (Vernacexpr.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
 
 type program_info = {
   prg_name: identifier;
@@ -342,7 +342,7 @@ type program_info = {
   prg_obligations: obligations;
   prg_deps : identifier list;
   prg_fixkind : fixpoint_kind option ;
-  prg_implicits : (Topconstr.explicitation * (bool * bool * bool)) list;
+  prg_implicits : (Constrexpr.explicitation * (bool * bool * bool)) list;
   prg_notations : notations ;
   prg_kind : definition_kind;
   prg_reduce : constr -> constr;
diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli
index df093ea43d..d052cc4412 100644
--- a/toplevel/obligations.mli
+++ b/toplevel/obligations.mli
@@ -70,21 +70,22 @@ val set_proofs_transparency : bool -> unit (* true = All transparent, false = Op
 val get_proofs_transparency : unit -> bool
 
 val add_definition : Names.identifier -> ?term:Term.constr -> Term.types -> 
-  ?implicits:(Topconstr.explicitation * (bool * bool * bool)) list ->
+  ?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list ->
   ?kind:Decl_kinds.definition_kind ->
   ?tactic:Proof_type.tactic ->
   ?reduce:(Term.constr -> Term.constr) ->
   ?hook:(unit Tacexpr.declaration_hook) -> obligation_info -> progress
 
-type notations = (Vernacexpr.lstring * Topconstr.constr_expr * Topconstr.scope_name option) list
+type notations =
+    (Vernacexpr.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
 
 type fixpoint_kind =
-  | IsFixpoint of (identifier located option * Topconstr.recursion_order_expr) list
+  | IsFixpoint of (identifier located option * Constrexpr.recursion_order_expr) list
   | IsCoFixpoint
 
 val add_mutual_definitions :
   (Names.identifier * Term.constr * Term.types *
-      (Topconstr.explicitation * (bool * bool * bool)) list * obligation_info) list ->
+      (Constrexpr.explicitation * (bool * bool * bool)) list * obligation_info) list ->
   ?tactic:Proof_type.tactic ->
   ?kind:Decl_kinds.definition_kind ->
   ?reduce:(Term.constr -> Term.constr) ->
@@ -92,7 +93,7 @@ val add_mutual_definitions :
   notations ->
   fixpoint_kind -> unit
 
-val obligation : int * Names.identifier option * Topconstr.constr_expr option ->
+val obligation : int * Names.identifier option * Constrexpr.constr_expr option ->
   Tacexpr.raw_tactic_expr option -> unit
 
 val next_obligation : Names.identifier option -> Tacexpr.raw_tactic_expr option -> unit
diff --git a/toplevel/record.ml b/toplevel/record.ml
index c6f620ae50..f4ef35e01b 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -25,6 +25,7 @@ open Safe_typing
 open Decl_kinds
 open Indtypes
 open Type_errors
+open Constrexpr
 open Topconstr
 
 (********** definition d'un record (structure) **************)
diff --git a/toplevel/record.mli b/toplevel/record.mli
index 45670f1fae..e2d56cfd87 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -10,7 +10,7 @@ open Names
 open Term
 open Sign
 open Vernacexpr
-open Topconstr
+open Constrexpr
 open Impargs
 open Libnames
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 6ac321e43d..73c05de3fc 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -28,7 +28,7 @@ open Libnames
 open Nametab
 open Vernacexpr
 open Decl_kinds
-open Topconstr
+open Constrexpr
 open Pretyping
 open Redexpr
 open Syntax_def
@@ -875,7 +875,7 @@ let vernac_reserve bl =
   let sb_decl = (fun (idl,c) ->
     let t = Constrintern.interp_type Evd.empty (Global.env()) c in
     let t = Detyping.detype false [] [] t in
-    let t = aconstr_of_glob_constr [] [] t in
+    let t = Topconstr.notation_constr_of_glob_constr [] [] t in
     Reserve.declare_reserved_type idl t)
   in List.iter sb_decl bl
 
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 704f06fb51..2e33f7fd37 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -10,7 +10,7 @@ open Names
 open Term
 open Vernacinterp
 open Vernacexpr
-open Topconstr
+open Constrexpr
 open Misctypes
 
 (** Vernacular entries *)