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

17 files changed, 60 insertions, 49 deletions

diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 17a4d98ad..d55363b17 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -13,7 +13,8 @@ open Util
 open Pcoq
 open Extend
 open Ppextend
-open Topconstr
+open Constrexpr
+open Notation_term
 open Genarg
 open Libnames
 open Nameops
@@ -108,7 +109,7 @@ let make_constr_action
   make ([],[],[]) (List.rev pil)
 
 let check_cases_pattern_env loc (env,envlist,hasbinders) =
-  if hasbinders then error_invalid_pattern_notation loc else (env,envlist)
+  if hasbinders then Topconstr.error_invalid_pattern_notation loc else (env,envlist)
 
 let make_cases_pattern_action
   (f : loc -> cases_pattern_notation_substitution -> cases_pattern_expr) pil =
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli
index c9f92b729..108f39eaa 100644
--- a/parsing/egrammar.mli
+++ b/parsing/egrammar.mli
@@ -10,7 +10,8 @@ open Compat
 open Errors
 open Pp
 open Names
-open Topconstr
+open Constrexpr
+open Notation_term
 open Pcoq
 open Extend
 open Vernacexpr
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index c8ca6cbab..1bc46f83f 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -14,7 +14,7 @@ open Glob_term
 open Term
 open Names
 open Libnames
-open Topconstr
+open Constrexpr
 open Util
 open Tok
 open Compat
@@ -31,7 +31,9 @@ let _ = List.iter Lexer.add_keyword constr_kw
 
 let mk_cast = function
     (c,(_,None)) -> c
-  | (c,(_,Some ty)) -> CCast(join_loc (constr_loc c) (constr_loc ty), c, CastConv ty)
+  | (c,(_,Some ty)) ->
+    let loc = join_loc (Topconstr.constr_loc c) (Topconstr.constr_loc ty)
+    in CCast(loc, c, CastConv ty)
 
 let binders_of_names l =
   List.map (fun (loc, na) ->
@@ -223,13 +225,15 @@ GEXTEND Gram
   ;
   binder_constr:
     [ [ forall; bl = open_binders; ","; c = operconstr LEVEL "200" ->
-          mkCProdN loc bl c
+          Topconstr.mkCProdN loc bl c
       | lambda; bl = open_binders; "=>"; c = operconstr LEVEL "200" ->
-          mkCLambdaN loc bl c
+          Topconstr.mkCLambdaN loc bl c
       | "let"; id=name; bl = binders; ty = type_cstr; ":=";
         c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" ->
-          let loc1 = join_loc (local_binders_loc bl) (constr_loc c1) in
-          CLetIn(loc,id,mkCLambdaN loc1 bl (mk_cast(c1,ty)),c2)
+          let loc1 =
+	    join_loc (Topconstr.local_binders_loc bl) (Topconstr.constr_loc c1)
+	  in
+          CLetIn(loc,id,Topconstr.mkCLambdaN loc1 bl (mk_cast(c1,ty)),c2)
       | "let"; fx = single_fix; "in"; c = operconstr LEVEL "200" ->
           let fixp = mk_single_fix fx in
           let (li,id) = match fixp with
@@ -338,7 +342,7 @@ GEXTEND Gram
         (match p with
           | CPatAtom (_, Some r) -> CPatCstr (loc, r, lp)
           | _ -> Errors.user_err_loc
-              (cases_pattern_expr_loc p, "compound_pattern",
+              (Topconstr.cases_pattern_expr_loc p, "compound_pattern",
                Pp.str "Constructor expected."))
       |"@"; r = Prim.reference; lp = LIST1 NEXT ->
         CPatCstrExpl (loc, r, lp) ]
@@ -391,7 +395,7 @@ GEXTEND Gram
       | id = name; idl = LIST0 name; bl = binders ->
           binders_of_names (id::idl) @ bl
       | id1 = name; ".."; id2 = name ->
-          [LocalRawAssum ([id1;(loc,Name ldots_var);id2],
+          [LocalRawAssum ([id1;(loc,Name Topconstr.ldots_var);id2],
 	                  Default Explicit,CHole (loc,None))]
       | bl = closed_binder; bl' = binders ->
 	  bl@bl'
@@ -412,7 +416,7 @@ GEXTEND Gram
       | "("; id=name; ":="; c=lconstr; ")" ->
           [LocalRawDef (id,c)]
       | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" ->
-          [LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv t))]
+          [LocalRawDef (id,CCast (join_loc (Topconstr.constr_loc t) loc,c, CastConv t))]
       | "{"; id=name; "}" ->
           [LocalRawAssum ([id],Default Implicit,CHole (loc, None))]
       | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" ->
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 811fd58ff..c8356b603 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -8,7 +8,7 @@
 
 open Pp
 open Util
-open Topconstr
+open Constrexpr
 open Glob_term
 open Tacexpr
 open Vernacexpr
diff --git a/parsing/g_obligations.ml4 b/parsing/g_obligations.ml4
index 8ec546ffd..339e0ca16 100644
--- a/parsing/g_obligations.ml4
+++ b/parsing/g_obligations.ml4
@@ -20,6 +20,7 @@ open Nameops
 open Reduction
 open Term
 open Libnames
+open Constrexpr
 open Topconstr
 
 (* We define new entries for programs, with the use of this module
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 6edb0bfc1..22a9e0d85 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -11,7 +11,7 @@ open Pp
 open Tactic
 open Util
 open Vernac_
-open Topconstr
+open Constrexpr
 open Vernacexpr
 open Locality
 open Prim
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 4c1d747ea..c373371d2 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -13,7 +13,7 @@ open Util
 open Tacexpr
 open Genredexpr
 open Genarg
-open Topconstr
+open Constrexpr
 open Libnames
 open Termops
 open Tok
@@ -129,7 +129,7 @@ let mk_cofix_tac (loc,id,bl,ann,ty) =
 (* Functions overloaded by quotifier *)
 let induction_arg_of_constr (c,lbind as clbind) =
   if lbind = NoBindings then
-    try ElimOnIdent (constr_loc c,snd(coerce_to_id c))
+    try ElimOnIdent (Topconstr.constr_loc c,snd(Topconstr.coerce_to_id c))
     with _ -> ElimOnConstr clbind
   else ElimOnConstr clbind
 
@@ -163,7 +163,7 @@ let rec mkCLambdaN_simple_loc loc bll c =
 let mkCLambdaN_simple bl c =
   if bl=[] then c
   else
-    let loc = join_loc (fst (List.hd (pi1 (List.hd bl)))) (constr_loc c) in
+    let loc = join_loc (fst (List.hd (pi1 (List.hd bl)))) (Topconstr.constr_loc c) in
     mkCLambdaN_simple_loc loc bl c
 
 let loc_of_ne_list l = join_loc (fst (List.hd l)) (fst (list_last l))
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 83c5e6f31..51088564b 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -12,6 +12,7 @@ open Tok
 open Errors
 open Util
 open Names
+open Constrexpr
 open Topconstr
 open Extend
 open Vernacexpr
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index e113bb711..886f91ea0 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -13,7 +13,7 @@ open Glob_term
 open Extend
 open Vernacexpr
 open Genarg
-open Topconstr
+open Constrexpr
 open Tacexpr
 open Libnames
 open Compat
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 6b2e206b6..d7e968ad4 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -15,6 +15,7 @@ open Names
 open Nameops
 open Libnames
 open Ppextend
+open Constrexpr
 open Topconstr
 open Term
 open Pattern
@@ -338,7 +339,7 @@ let pr_guard_annot pr_aux bl (n,ro) =
   match n with
     | None -> mt ()
     | Some (loc, id) ->
-      match (ro : Topconstr.recursion_order_expr) with
+      match (ro : Constrexpr.recursion_order_expr) with
 	| CStructRec ->
 	  let names_of_binder = function
 	    | LocalRawAssum (nal,_,_) -> nal
diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli
index 390869cf7..88e4e55dc 100644
--- a/parsing/ppconstr.mli
+++ b/parsing/ppconstr.mli
@@ -12,7 +12,7 @@ open Term
 open Libnames
 open Pcoq
 open Glob_term
-open Topconstr
+open Constrexpr
 open Names
 open Errors
 open Util
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 5d03b6028..bbfecac8f 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -13,7 +13,7 @@ open Errors
 open Util
 open Tacexpr
 open Glob_term
-open Topconstr
+open Constrexpr
 open Genarg
 open Libnames
 open Pattern
@@ -294,7 +294,7 @@ let pr_extend prc prlc prtac prpat =
 let strip_prod_binders_expr n ty =
   let rec strip_ty acc n ty =
     match ty with
-        Topconstr.CProdN(_,bll,a) ->
+        Constrexpr.CProdN(_,bll,a) ->
           let nb =
             List.fold_left (fun i (nal,_,_) -> i + List.length nal) 0 bll in
 	  let bll = List.map (fun (x, _, y) -> x, y) bll in
diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli
index afcc83c68..7a5c43531 100644
--- a/parsing/pptactic.mli
+++ b/parsing/pptactic.mli
@@ -11,7 +11,7 @@ open Genarg
 open Tacexpr
 open Pretyping
 open Proof_type
-open Topconstr
+open Constrexpr
 open Glob_term
 open Pattern
 open Ppextend
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 9f0cc4c03..2cbc0222b 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -22,6 +22,7 @@ open Genarg
 open Pcoq
 open Libnames
 open Ppextend
+open Constrexpr
 open Topconstr
 open Decl_kinds
 open Tacinterp
@@ -752,7 +753,7 @@ let rec pr_vernac = function
 	++ (if redef then str" ::=" else str" :=") ++ brk(1,1) ++
 	let idl = List.map Option.get (List.filter (fun x -> not (x=None)) idl)in
         pr_raw_tactic_env
-	  (idl @ List.map coerce_reference_to_id
+	  (idl @ List.map Topconstr.coerce_reference_to_id
 	    (List.map (fun (x, _, _) -> x) (List.filter (fun (_, redef, _) -> not redef) l)))
 	  (Global.env())
 	  body in
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 5dbef1fe5..d90e655b1 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -44,7 +44,7 @@ type object_pr = {
   print_library_entry       : bool -> (object_name * Lib.node) -> std_ppcmds option;
   print_context             : bool -> int option -> Lib.library_segment -> std_ppcmds;
   print_typed_value_in_env  : Environ.env -> Term.constr * Term.types -> Pp.std_ppcmds;
-  print_eval                : Reductionops.reduction_function -> env -> Evd.evar_map -> Topconstr.constr_expr -> unsafe_judgment -> std_ppcmds;
+  print_eval                : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> unsafe_judgment -> std_ppcmds;
 }
 
 let gallina_print_module  = print_module
@@ -435,7 +435,7 @@ let gallina_print_constant_with_infos sp =
 let gallina_print_syntactic_def kn =
   let qid = Nametab.shortest_qualid_of_syndef Idset.empty kn
   and (vars,a) = Syntax_def.search_syntactic_definition kn in
-  let c = Topconstr.glob_constr_of_aconstr dummy_loc a in
+  let c = Topconstr.glob_constr_of_notation_constr dummy_loc a in
   hov 2
     (hov 4
        (str "Notation " ++ pr_qualid qid ++
diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli
index b3271d141..122da7ebf 100644
--- a/parsing/prettyp.mli
+++ b/parsing/prettyp.mli
@@ -33,7 +33,8 @@ val print_sec_context_typ : reference -> std_ppcmds
 val print_judgment : env -> unsafe_judgment -> std_ppcmds
 val print_safe_judgment : env -> Safe_typing.judgment -> std_ppcmds
 val print_eval :
-  reduction_function -> env -> Evd.evar_map -> Topconstr.constr_expr -> unsafe_judgment -> std_ppcmds
+  reduction_function -> env -> Evd.evar_map ->
+    Constrexpr.constr_expr -> unsafe_judgment -> std_ppcmds
 
 val print_name : reference or_by_notation -> std_ppcmds
 val print_opaque_name : reference -> std_ppcmds
@@ -68,7 +69,7 @@ type object_pr = {
   print_library_entry       : bool -> (object_name * Lib.node) -> std_ppcmds option;
   print_context             : bool -> int option -> Lib.library_segment -> std_ppcmds;
   print_typed_value_in_env  : Environ.env -> Term.constr * Term.types -> Pp.std_ppcmds;
-  print_eval                : reduction_function -> env -> Evd.evar_map -> Topconstr.constr_expr -> unsafe_judgment -> std_ppcmds
+  print_eval                : reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> unsafe_judgment -> std_ppcmds
 }
 
 val set_object_pr : object_pr -> unit
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index a75d1f6cc..cb4fad6f5 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -122,40 +122,40 @@ let mlexpr_of_red_flags {
 } >>
 
 let mlexpr_of_explicitation = function
-  | Topconstr.ExplByName id -> <:expr< Topconstr.ExplByName $mlexpr_of_ident id$ >>
-  | Topconstr.ExplByPos (n,_id) -> <:expr< Topconstr.ExplByPos $mlexpr_of_int n$ >>
+  | Constrexpr.ExplByName id -> <:expr< Constrexpr.ExplByName $mlexpr_of_ident id$ >>
+  | Constrexpr.ExplByPos (n,_id) -> <:expr< Constrexpr.ExplByPos $mlexpr_of_int n$ >>
 
 let mlexpr_of_binding_kind = function
   | Decl_kinds.Implicit -> <:expr< Decl_kinds.Implicit >>
   | Decl_kinds.Explicit -> <:expr< Decl_kinds.Explicit >>
 
 let mlexpr_of_binder_kind = function
-  | Topconstr.Default b -> <:expr< Topconstr.Default $mlexpr_of_binding_kind b$ >>
-  | Topconstr.Generalized (b,b',b'') ->
-      <:expr< Topconstr.TypeClass $mlexpr_of_binding_kind b$
+  | Constrexpr.Default b -> <:expr< Constrexpr.Default $mlexpr_of_binding_kind b$ >>
+  | Constrexpr.Generalized (b,b',b'') ->
+      <:expr< Constrexpr.TypeClass $mlexpr_of_binding_kind b$
 	$mlexpr_of_binding_kind b'$ $mlexpr_of_bool b''$ >>
 
 let rec mlexpr_of_constr = function
-  | Topconstr.CRef (Libnames.Ident (loc,id)) when is_meta (string_of_id id) ->
+  | Constrexpr.CRef (Libnames.Ident (loc,id)) when is_meta (string_of_id id) ->
       anti loc (string_of_id id)
-  | Topconstr.CRef r -> <:expr< Topconstr.CRef $mlexpr_of_reference r$ >>
-  | Topconstr.CFix (loc,_,_) -> failwith "mlexpr_of_constr: TODO"
-  | Topconstr.CCoFix (loc,_,_) -> failwith "mlexpr_of_constr: TODO"
-  | Topconstr.CProdN (loc,l,a) -> <:expr< Topconstr.CProdN $dloc$ $mlexpr_of_list
+  | Constrexpr.CRef r -> <:expr< Constrexpr.CRef $mlexpr_of_reference r$ >>
+  | Constrexpr.CFix (loc,_,_) -> failwith "mlexpr_of_constr: TODO"
+  | Constrexpr.CCoFix (loc,_,_) -> failwith "mlexpr_of_constr: TODO"
+  | Constrexpr.CProdN (loc,l,a) -> <:expr< Constrexpr.CProdN $dloc$ $mlexpr_of_list
       (mlexpr_of_triple (mlexpr_of_list (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_name)) mlexpr_of_binder_kind mlexpr_of_constr) l$ $mlexpr_of_constr a$ >>
-  | Topconstr.CLambdaN (loc,l,a) -> <:expr< Topconstr.CLambdaN $dloc$ $mlexpr_of_list (mlexpr_of_triple (mlexpr_of_list (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_name)) mlexpr_of_binder_kind mlexpr_of_constr) l$ $mlexpr_of_constr a$ >>
-  | Topconstr.CLetIn (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO"
-  | Topconstr.CAppExpl (loc,a,l) -> <:expr< Topconstr.CAppExpl $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_reference a$ $mlexpr_of_list mlexpr_of_constr l$ >>
-  | Topconstr.CApp (loc,a,l) -> <:expr< Topconstr.CApp $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_constr a$ $mlexpr_of_list (mlexpr_of_pair mlexpr_of_constr (mlexpr_of_option (mlexpr_of_located mlexpr_of_explicitation))) l$ >>
-  | Topconstr.CCases (loc,_,_,_,_) -> failwith "mlexpr_of_constr: TODO"
-  | Topconstr.CHole (loc, None) -> <:expr< Topconstr.CHole $dloc$ None >>
-  | Topconstr.CHole (loc, Some _) -> failwith "mlexpr_of_constr: TODO CHole (Some _)"
-  | Topconstr.CNotation(_,ntn,(subst,substl,[])) ->
-      <:expr< Topconstr.CNotation $dloc$ $mlexpr_of_string ntn$
+  | Constrexpr.CLambdaN (loc,l,a) -> <:expr< Constrexpr.CLambdaN $dloc$ $mlexpr_of_list (mlexpr_of_triple (mlexpr_of_list (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_name)) mlexpr_of_binder_kind mlexpr_of_constr) l$ $mlexpr_of_constr a$ >>
+  | Constrexpr.CLetIn (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO"
+  | Constrexpr.CAppExpl (loc,a,l) -> <:expr< Constrexpr.CAppExpl $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_reference a$ $mlexpr_of_list mlexpr_of_constr l$ >>
+  | Constrexpr.CApp (loc,a,l) -> <:expr< Constrexpr.CApp $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_constr a$ $mlexpr_of_list (mlexpr_of_pair mlexpr_of_constr (mlexpr_of_option (mlexpr_of_located mlexpr_of_explicitation))) l$ >>
+  | Constrexpr.CCases (loc,_,_,_,_) -> failwith "mlexpr_of_constr: TODO"
+  | Constrexpr.CHole (loc, None) -> <:expr< Constrexpr.CHole $dloc$ None >>
+  | Constrexpr.CHole (loc, Some _) -> failwith "mlexpr_of_constr: TODO CHole (Some _)"
+  | Constrexpr.CNotation(_,ntn,(subst,substl,[])) ->
+      <:expr< Constrexpr.CNotation $dloc$ $mlexpr_of_string ntn$
               ($mlexpr_of_list mlexpr_of_constr subst$,
                $mlexpr_of_list (mlexpr_of_list mlexpr_of_constr) substl$,[]) >>
-  | Topconstr.CPatVar (loc,n) ->
-      <:expr< Topconstr.CPatVar $dloc$ $mlexpr_of_pair mlexpr_of_bool mlexpr_of_ident n$ >>
+  | Constrexpr.CPatVar (loc,n) ->
+      <:expr< Constrexpr.CPatVar $dloc$ $mlexpr_of_pair mlexpr_of_bool mlexpr_of_ident n$ >>
   | _ -> failwith "mlexpr_of_constr: TODO"
 
 let mlexpr_of_occ_constr =