Restructuration des points d'entrée de Pretyping et Constrintern

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

12 files changed, 199 insertions, 276 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 06d11e6653..6eacde19ad 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -247,7 +247,7 @@ let set_var_scope loc id (_,scopt,scopes) varscopes =
    [vars2] is the set of global variables, env is the set of variables
    abstracted until this point *)
 
-let intern_var (env,_,_ as genv) (ltacvars,vars2,vars3,_,impls) loc id =
+let intern_var (env,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) loc id =
   let (vars1,unbndltacvars) = ltacvars in
   (* Is [id] an inductive type potentially with implicit *)
   try
@@ -285,7 +285,7 @@ let intern_var (env,_,_ as genv) (ltacvars,vars2,vars3,_,impls) loc id =
     (* [id] a goal variable *)
     RVar (loc,id), [], [], []
 
-let find_appl_head_data (_,_,_,_,impls) = function
+let find_appl_head_data (_,_,_,(_,impls)) = function
   | RRef (_,ref) as x -> x,implicits_of_global ref,find_arguments_scope ref,[]
   | x -> x,[],[],[]
 
@@ -334,7 +334,7 @@ let intern_reference env lvar = function
 	else raise e
 
 let interp_reference vars r =
-  let (r,_,_,_) = intern_reference (Idset.empty,None,[]) (vars,[],[],[],[]) r 
+  let r,_,_,_ = intern_reference (Idset.empty,None,[]) (vars,[],[],([],[])) r 
   in r
 
 let apply_scope_env (ids,_,scopes) = function
@@ -628,7 +628,7 @@ let locate_if_isevar loc na = function
       with Not_found -> RHole (loc, Evd.BinderType na))
   | x -> x
 
-let check_hidden_implicit_parameters id (_,_,_,indnames,_) =
+let check_hidden_implicit_parameters id (_,_,_,(indnames,_)) =
   if List.mem id indnames then
     errorlabstrm "" (str "A parameter or name of an inductive type " ++
     pr_id id ++ str " must not be used as a bound variable in the type \
@@ -919,7 +919,7 @@ let internalise sigma env allow_soapp lvar c =
     | CPatVar (loc, (false,n)) when Options.do_translate () ->
 	RVar (loc, n)
     | CPatVar (loc, (false,n)) ->
-        if List.mem n (fst (let (a,_,_,_,_) = lvar in a)) & !Options.v7 then
+        if List.mem n (fst (let (a,_,_,_) = lvar in a)) & !Options.v7 then
 	  RVar (loc, n)
 	else
           error_unbound_patvar loc n
@@ -1063,113 +1063,53 @@ let extract_ids env =
     (Termops.ids_of_rel_context (Environ.rel_context env))
     Idset.empty
 
-let interp_rawconstr_gen_with_implicits isarity sigma env (indpars,impls) allow_soapp ltacvar c =
+let intern_gen isarity sigma env
+               ?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[]))
+               c =
   let tmp_scope = if isarity then Some Notation.type_scope else None in
   internalise sigma (extract_ids env, tmp_scope,[])
-    allow_soapp (ltacvar,Environ.named_context env, [], indpars, impls) c
+    allow_soapp (ltacvars,Environ.named_context env, [], impls) c
 
-let interp_rawconstr_gen isarity sigma env allow_soapp ltacvar c =
-  interp_rawconstr_gen_with_implicits isarity sigma env ([],[]) allow_soapp ltacvar c
+let intern_constr sigma env c = intern_gen true sigma env c 
 
-let interp_rawconstr sigma env c =
-  interp_rawconstr_gen false sigma env false ([],[]) c
-
-let interp_rawtype sigma env c =
-  interp_rawconstr_gen true sigma env false ([],[]) c
-
-let interp_rawtype_with_implicits sigma env impls c =
-  interp_rawconstr_gen_with_implicits true sigma env impls false ([],[]) c
-
-let interp_rawconstr_with_implicits sigma env vars impls c =
-  interp_rawconstr_gen_with_implicits false sigma env ([],impls) false
-    (vars,[]) c
-
-(*
-(* The same as interp_rawconstr but with a list of variables which must not be
-   globalized *)
-
-let interp_rawconstr_wo_glob sigma env lvar c =
-  interp_rawconstr_gen sigma env [] (Some []) lvar c
-*)
+let intern_ltac isarity ltacvars sigma env c =
+  intern_gen isarity sigma env ~ltacvars:ltacvars c
 
 (*********************************************************************)
 (* Functions to parse and interpret constructions *)
 
-let interp_constr sigma env c =
-  understand sigma env (interp_rawconstr sigma env c)
-
-let interp_openconstr sigma env c =
-  understand_gen_tcc sigma env [] None (interp_rawconstr sigma env c)
-
-(*
-let interp_casted_openconstr sigma env c typ =
-  understand_gen_tcc sigma env [] (Some typ) (interp_rawconstr sigma env c)
-*)
-
-let interp_type sigma env c =
-  understand_type sigma env (interp_rawtype sigma env c)
+let interp_gen kind sigma env 
+               ?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[]))
+               c =
+  understand_gen kind sigma env 
+    (intern_gen (kind=IsType) ~impls ~allow_soapp ~ltacvars sigma env c)
 
-let interp_binder sigma env na t =
-  let t = interp_rawtype sigma env t in
-  understand_type sigma env (locate_if_isevar (loc_of_rawconstr t) na t)
-
-let interp_type_with_implicits sigma env impls c =
-  understand_type sigma env (interp_rawtype_with_implicits sigma env impls c)
+let interp_constr sigma env c =
+  interp_gen (OfType None) sigma env c 
 
-let judgment_of_rawconstr sigma env c =
-  understand_judgment sigma env (interp_rawconstr sigma env c)
+let interp_type sigma env ?(impls=([],[])) c =
+  interp_gen IsType sigma env ~impls c
 
-let type_judgment_of_rawconstr sigma env c =
-  understand_type_judgment sigma env (interp_rawconstr sigma env c)
+let interp_casted_constr sigma env ?(impls=([],[])) c typ =
+  interp_gen (OfType (Some typ)) sigma env ~impls c 
 
-(* To retype a list of key*constr with undefined key *)
-let retype_list sigma env lst =
-  List.fold_right (fun (x,csr) a ->
-    try (x,Retyping.get_judgment_of env sigma csr)::a with
-    | Anomaly _ -> a) lst []
+let interp_open_constr sigma env c =
+  understand_tcc sigma env (intern_constr sigma env c)
 
-(*  List.map (fun (x,csr) -> (x,Retyping.get_judgment_of env sigma csr)) lst*)
+let interp_constr_judgment sigma env c =
+  understand_judgment sigma env (intern_constr sigma env c)
 
 type ltac_sign = identifier list * unbound_ltac_var_map
-type ltac_env = (identifier * Term.constr) list * unbound_ltac_var_map
-
-(* Interprets a constr according to two lists *)
-(* of instantiations (variables and metas)    *)
-(* Note: typ is retyped *)
-let interp_constr_gen sigma env (ltacvars,unbndltacvars) c exptyp =
-  let c = interp_rawconstr_gen false sigma env false
-    (List.map fst ltacvars,unbndltacvars) c in
-  let typs = retype_list sigma env ltacvars in
-  understand_gen_ltac sigma env (typs,[]) exptyp c
-
-(*Interprets a casted constr according to two lists of instantiations
-  (variables and metas)*)
-let interp_openconstr_gen sigma env (ltacvars,unbndltacvars) c exptyp =
-  let c = interp_rawconstr_gen false sigma env false
-    (List.map fst ltacvars,unbndltacvars) c in
-  let typs = retype_list sigma env ltacvars in
-  understand_gen_tcc sigma env typs exptyp c
-
-let interp_casted_constr sigma env c typ = 
-  understand_gen sigma env [] (Some typ) (interp_rawconstr sigma env c)
-
-let interp_casted_constr_with_implicits sigma env impls c typ =
-  understand_gen sigma env [] (Some typ) 
-    (interp_rawconstr_with_implicits sigma env [] impls c)
-
-let interp_constrpattern_gen sigma env ltacvar c =
-  let c = interp_rawconstr_gen false sigma env true (ltacvar,[]) c in
-  pattern_of_rawconstr c
 
 let interp_constrpattern sigma env c =
-  interp_constrpattern_gen sigma env [] c
+  pattern_of_rawconstr (intern_constr sigma env c)
 
 let interp_aconstr impls vars a =
   let env = Global.env () in
   (* [vl] is intended to remember the scope of the free variables of [a] *)
   let vl = List.map (fun id -> (id,ref None)) vars in
   let c = internalise Evd.empty (extract_ids env, None, [])
-    false (([],[]),Environ.named_context env,vl,[],impls) a in
+    false (([],[]),Environ.named_context env,vl,([],impls)) a in
   (* Translate and check that [c] has all its free variables bound in [vars] *)
   let a = aconstr_of_rawconstr vars c in
   (* Returns [a] and the ordered list of variables with their scopes *)
@@ -1178,6 +1118,33 @@ let interp_aconstr impls vars a =
     (fun (id,r) -> (id,match !r with None -> None,[] | Some (a,l) -> a,l)) vl,
   a
 
+(* Interpret binders and contexts  *)
+
+let interp_binder sigma env na t =
+  let t = intern_gen true sigma env t in
+  understand_type sigma env (locate_if_isevar (loc_of_rawconstr t) na t)
+
+open Environ
+open Term
+
+let interp_context sigma env params = 
+  List.fold_left
+    (fun (env,params) d -> match d with
+      | LocalRawAssum ([_,na],(CHole _ as t)) ->
+	  let t = interp_binder sigma env na t in
+	  let d = (na,None,t) in
+	  (push_rel d env, d::params)
+      | LocalRawAssum (nal,t) ->
+	  let t = interp_type sigma env t in
+	  let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal in
+	  let ctx = List.rev ctx in
+	  (push_rel_context ctx env, ctx@params)
+      | LocalRawDef ((_,na),c) ->
+	  let c = interp_constr_judgment sigma env c in
+	  let d = (na, Some c.uj_val, c.uj_type) in
+	  (push_rel d env,d::params))
+    (env,[]) params
+
 (**********************************************************************)
 (* Locating reference, possibly via an abbreviation *)
 
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 757f02a466..08de85d87b 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -35,7 +35,11 @@ open Pretyping
 *)
 
 (* To interpret implicits and arg scopes of recursive variables in
-   inductive types and recursive definitions *)
+   inductive types and recursive definitions; mention of a list of
+   implicits arguments in the ``rel'' part of [env]; the second
+   argument associates a list of implicit positions and scopes to
+   identifiers declared in the [rel_context] of [env] *)
+
 type var_internalisation_data =
     identifier list * Impargs.implicits_list * scope_name option list
 
@@ -43,61 +47,55 @@ type implicits_env = (identifier * var_internalisation_data) list
 type full_implicits_env = identifier list * implicits_env
 
 type ltac_sign = identifier list * unbound_ltac_var_map
-type ltac_env = (identifier * constr) list * unbound_ltac_var_map
-
-(* Interprets global names, including syntactic defs and section variables *)
-val interp_rawconstr     : evar_map -> env -> constr_expr -> rawconstr
-val interp_rawconstr_gen : bool -> evar_map -> env -> 
-    bool -> ltac_sign -> constr_expr -> rawconstr
-
-(*s Composing the translation with typing *)
-val interp_constr        : evar_map -> env -> constr_expr -> constr
-val interp_casted_constr : evar_map -> env -> constr_expr -> types -> constr
-val interp_type          : evar_map -> env -> constr_expr -> types
-val interp_binder        : evar_map -> env -> name -> constr_expr -> types
-val interp_openconstr    : evar_map -> env -> constr_expr -> evar_map * constr
-
-(* [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] *)
-val interp_type_with_implicits : 
-  evar_map -> env -> full_implicits_env -> constr_expr -> types
-
-val interp_casted_constr_with_implicits :
-  evar_map -> env -> implicits_env -> constr_expr -> types -> constr
-
-val interp_rawconstr_with_implicits :
-  evar_map -> env -> identifier list -> implicits_env -> constr_expr -> 
-    rawconstr
-
-(*s Build a judgement from *)
-val judgment_of_rawconstr : evar_map -> env -> constr_expr -> unsafe_judgment
-val type_judgment_of_rawconstr :
-  evar_map -> env -> constr_expr -> unsafe_type_judgment
-
-(* Interprets a constr according to two lists of instantiations (variables and
-  metas), possibly casting it*)
-val interp_constr_gen     :
-  evar_map -> env -> ltac_env -> constr_expr -> constr option ->
-    evar_defs * constr
-
-(* Interprets a constr according to two lists of instantiations (variables and
-  metas), possibly casting it, and turning unresolved evar into metas*)
-val interp_openconstr_gen     :
-  evar_map -> env -> ltac_env ->
-    constr_expr -> constr option -> evar_map * constr
-
-(* Interprets constr patterns according to a list of instantiations
-  (variables)*)
-val interp_constrpattern_gen : evar_map -> env -> identifier list ->
-  constr_expr -> patvar list * constr_pattern
+
+(*s Internalisation performs interpretation of global names and notations *)
+
+val intern_constr : evar_map -> env -> constr_expr -> rawconstr
+
+val intern_gen : bool -> evar_map -> env ->
+  ?impls:full_implicits_env -> ?allow_soapp:bool -> ?ltacvars:ltac_sign ->
+  constr_expr -> rawconstr
+
+(*s Composing internalisation with pretyping *)
+
+(* Main interpretation function *)
+
+val interp_gen : typing_constraint -> evar_map -> env ->
+  ?impls:full_implicits_env -> ?allow_soapp:bool -> ?ltacvars:ltac_sign ->
+  constr_expr -> constr
+
+(* Particular instances *)
+
+val interp_constr : evar_map -> env -> 
+  constr_expr -> constr
+
+val interp_casted_constr : evar_map -> env -> ?impls:full_implicits_env -> 
+  constr_expr -> types -> constr
+
+val interp_type : evar_map -> env -> ?impls:full_implicits_env -> 
+  constr_expr -> types
+
+val interp_open_constr   : evar_map -> env -> constr_expr -> evar_map * constr
+
+(*s Build a judgment  *)
+
+val interp_constr_judgment : evar_map -> env -> constr_expr -> unsafe_judgment
+
+(* Interprets constr patterns *)
 
 val interp_constrpattern : 
   evar_map -> env -> constr_expr -> patvar list * constr_pattern
 
 val interp_reference : ltac_sign -> reference -> rawconstr
 
+(* Interpret binders *)
+
+val interp_binder  : evar_map -> env -> name -> constr_expr -> types
+
+(* Interpret contexts: returns extended env and context *)
+
+val interp_context : evar_map -> env -> local_binder list -> env * rel_context
+
 (* Locating references of constructions, possibly via a syntactic definition *)
 
 val locate_reference : qualid -> global_reference
@@ -107,6 +105,7 @@ val global_reference : identifier -> constr
 val global_reference_in_absolute_module : dir_path -> identifier -> constr
 
 (* Interprets into a abbreviatable constr *)
+
 val interp_aconstr : implicits_env -> identifier list -> constr_expr ->
   interpretation
 
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index c5ff391a0b..49b29d1dec 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -504,7 +504,7 @@ GEXTEND Gram
     [ [ "<<" ; a = Prim.ast; ">>" -> a 
       | a = Constr.constr -> 
 	  Termast.ast_of_rawconstr 
-	  (Constrintern.interp_rawconstr Evd.empty (Global.env()) a)
+	  (Constrintern.intern_constr Evd.empty (Global.env()) a)
     ] ]
   ; 
   action:
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index c0e20c399e..0baaa98198 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -956,13 +956,16 @@ and pretype_type valcon env isevars lvar = function
                 (loc_of_rawconstr c) env (evars_of !isevars) tj.utj_val v
 
 
-let unsafe_infer tycon isevars env lvar constr =
-  let j = pretype tycon env isevars lvar constr in
-  j_nf_evar (evars_of !isevars) j
+type typing_constraint = OfType of types option | IsType
 
-let unsafe_infer_type valcon isevars env lvar constr =
-  let tj = pretype_type valcon env isevars lvar constr in
-  tj_nf_evar (evars_of !isevars) tj
+let pretype_gen isevars env lvar kind c =
+  let c' = match kind with
+  | OfType exptyp ->
+    let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in
+    (pretype tycon env isevars lvar c).uj_val
+  | IsType ->
+    (pretype_type empty_valcon env isevars lvar c).utj_val in
+  nf_evar (evars_of !isevars) c'
 
 (* [check_evars] fails if some unresolved evar remains *)
 (* it assumes that the defined existentials have already been substituted
@@ -998,52 +1001,43 @@ let check_evars env initial_sigma isevars c =
        retourne aussi le nouveau sigma...
 *)
 
+let understand_judgment sigma env c =
+  let isevars = ref (create_evar_defs sigma) in
+  let j = pretype empty_tycon env isevars ([],[]) c in
+  let j = j_nf_evar (evars_of !isevars) j in
+  check_evars env sigma isevars (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
+  j
+
 (* Raw calls to the unsafe inference machine: boolean says if we must
    fail on unresolved evars; the unsafe_judgment list allows us to
    extend env with some bindings *)
 
-let ise_infer_gen fail_evar sigma env lvar exptyp c =
-  let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in
-  let isevars = ref (create_evar_defs sigma) in
-  let j = unsafe_infer tycon isevars env lvar c in
-  if fail_evar then 
-    check_evars env sigma isevars (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
-  (!isevars, j)
-
-let ise_infer_type_gen fail_evar sigma env lvar c =
+let ise_pretype_gen fail_evar sigma env lvar kind c =
   let isevars = ref (create_evar_defs sigma) in
-  let tj = unsafe_infer_type empty_valcon isevars env lvar c in
-  if fail_evar then check_evars env sigma isevars tj.utj_val;
-  (!isevars, tj)
+  let c = pretype_gen isevars env lvar kind c in
+  if fail_evar then check_evars env sigma isevars c;
+  (!isevars, c)
 
 (** Entry points of the high-level type synthesis algorithm *)
 
 type var_map = (identifier * unsafe_judgment) list
 type unbound_ltac_var_map = (identifier * identifier option) list
 
-let understand_judgment sigma env c =
-  snd (ise_infer_gen true sigma env ([],[]) None c)
-
-let understand_type_judgment sigma env c =
-  snd (ise_infer_type_gen true sigma env ([],[]) c)
+let understand_gen kind sigma env c =
+  snd (ise_pretype_gen true sigma env ([],[]) kind c)
 
-let understand sigma env c =
-  (understand_judgment sigma env c).uj_val
+let understand sigma env ?expected_type:exptyp c =
+  snd (ise_pretype_gen true sigma env ([],[]) (OfType exptyp) c)
 
 let understand_type sigma env c =
-  (understand_type_judgment sigma env c).utj_val
-
-let understand_gen_ltac sigma env lvar ~expected_type:exptyp c =
-  let evars,j = ise_infer_gen false sigma env lvar exptyp c in
-  (evars, j.uj_val)
+  snd (ise_pretype_gen true sigma env ([],[]) IsType c)
 
-let understand_gen sigma env lvar ~expected_type:exptyp c =
-  let _, c = ise_infer_gen true sigma env (lvar,[]) exptyp c in
-  c.uj_val
+let understand_ltac sigma env lvar kind c =
+  ise_pretype_gen false sigma env lvar kind c
 
-let understand_gen_tcc sigma env lvar ~expected_type:exptyp c =
-  let evars,j = ise_infer_gen false sigma env (lvar,[]) exptyp c in
-  evars_of evars, j.uj_val
+let understand_tcc sigma env ?expected_type:exptyp c =
+  let evars,c = ise_pretype_gen false sigma env ([],[]) (OfType exptyp) c in
+  evars_of evars,c
 
 (** Miscellaneous interpretation functions *)
 
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 80a9529c8a..d07b83ebac 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -18,49 +18,54 @@ open Rawterm
 open Evarutil
 (*i*)
 
+type typing_constraint = OfType of types option | IsType
+
+(* Generic call to the interpreter from rawconstr to open_constr, leaving
+   unresolved holes as evars and returning the typing contexts of
+   these evars. Work as [understand_gen] for the rest. *)
+
+val understand_tcc :
+  evar_map -> env -> ?expected_type:types -> rawconstr -> open_constr
+
+(* More general entry point with evars from ltac *)
+
 type var_map = (identifier * unsafe_judgment) list
 type unbound_ltac_var_map = (identifier * identifier option) list
 
 (* Generic call to the interpreter from rawconstr to constr, failing
    unresolved holes in the rawterm cannot be instantiated.
 
-   In [understand_gen sigma env varmap typopt raw],
+   In [understand_ltac sigma env ltac_env constraint c],
 
    sigma : initial set of existential variables (typically dependent subgoals)
-   varmap : partial subtitution of variables (used for the tactic language)
-   metamap : partial subtitution of meta (used for the tactic language)
-   typopt : is not None, this is the expected type for raw (used to define evars)
+   ltac_env : partial substitution of variables (used for the tactic language)
+   constraint : tell if interpreted as a possibly constrained term or a type 
 *)
-val understand_gen :
-  evar_map -> env -> var_map
-    -> expected_type:(constr option) -> rawconstr -> constr
-
-(* Generic call to the interpreter from rawconstr to constr, leaving
-   unresolved holes as evars and returning the typing contexts of
-   these evars. Work as [understand_gen] for the rest. *)
-val understand_gen_tcc :
-  evar_map -> env -> var_map
-    -> expected_type:(constr option) -> rawconstr -> open_constr
 
-(* More general entry point with evars from ltac *)
-val understand_gen_ltac :
-  evar_map -> env -> var_map * unbound_ltac_var_map
-    -> expected_type:(constr option) -> rawconstr -> evar_defs * constr
+val understand_ltac :
+  evar_map -> env -> var_map * unbound_ltac_var_map ->
+    typing_constraint -> rawconstr -> evar_defs * constr
 
 (* Standard call to get a constr from a rawconstr, resolving implicit args *)
-val understand : evar_map -> env -> rawconstr -> constr
+
+val understand : evar_map -> env -> ?expected_type:Term.types ->
+  rawconstr -> constr
 
 (* Idem but the rawconstr is intended to be a type *)
+
 val understand_type : evar_map -> env -> rawconstr -> constr
 
+(* A generalization of the two previous case *)
+
+val understand_gen : typing_constraint -> evar_map -> env -> 
+  rawconstr -> constr
+
 (* Idem but returns the judgment of the understood term *)
-val understand_judgment : evar_map -> env -> rawconstr -> unsafe_judgment
 
-(* Idem but returns the judgment of the understood type *)
-val understand_type_judgment : evar_map -> env -> rawconstr 
-  -> unsafe_type_judgment
+val understand_judgment : evar_map -> env -> rawconstr -> unsafe_judgment
 
 (* To embed constr in rawconstr *)
+
 val constr_in : constr -> Dyn.t
 val constr_out : Dyn.t -> constr
 
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 3db11ce390..1591d43c92 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -28,8 +28,8 @@ let w_refine env ev rawc evd =
   let e_info = Evd.map (evars_of evd) ev in
   let env = Evd.evar_env e_info in
   let sigma,typed_c = 
-    Pretyping.understand_gen_tcc (evars_of evd) env [] 
-      (Some e_info.evar_concl) rawc in
+    Pretyping.understand_tcc (evars_of evd) env 
+      ~expected_type:e_info.evar_concl rawc in
   evar_define ev typed_c (evars_reset_evd sigma evd)
 
 (* vernac command Existential *)
@@ -43,7 +43,7 @@ let instantiate_pf_com n com pfts =
     with Failure _ -> 
       error "not so many uninstantiated existential variables" in 
   let env = Evd.evar_env evi in
-  let rawc = Constrintern.interp_rawconstr sigma env com in 
+  let rawc = Constrintern.intern_constr sigma env com in 
   let evd = create_evar_defs sigma in
   let evd' = w_refine env sp rawc evd in
   change_constraints_pftreestate (evars_of evd') pfts
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 7ac7b185b7..adb18daa7a 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -79,10 +79,6 @@ let pf_interp_constr gls c =
   let evc = project gls in 
   Constrintern.interp_constr evc (pf_env gls) c
 
-let pf_interp_openconstr gls c =
-  let evc = project gls in 
-  Constrintern.interp_openconstr evc (pf_env gls) c
-
 let pf_interp_type gls c =
   let evc = project gls in 
   Constrintern.interp_type evc (pf_env gls) c
diff --git a/toplevel/command.ml b/toplevel/command.ml
index f64bae5a19..5fc9454388 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -42,19 +42,19 @@ open Notation
 let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,a,b))
 let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,a,b))
 
-let rec abstract_rawconstr c = function
+let rec abstract_constr_expr c = function
   | [] -> c
-  | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_rawconstr c bl)
+  | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl)
   | LocalRawAssum (idl,t)::bl ->
       List.fold_right (fun x b -> mkLambdaC([x],t,b)) idl
-        (abstract_rawconstr c bl)
+        (abstract_constr_expr c bl)
 
-let rec generalize_rawconstr c = function
+let rec generalize_constr_expr c = function
   | [] -> c
-  | LocalRawDef (x,b)::bl -> mkLetInC(x,b,generalize_rawconstr c bl)
+  | LocalRawDef (x,b)::bl -> mkLetInC(x,b,generalize_constr_expr c bl)
   | LocalRawAssum (idl,t)::bl ->
       List.fold_right (fun x b -> mkProdC([x],t,b)) idl
-        (generalize_rawconstr c bl)
+        (generalize_constr_expr c bl)
 
 let rec length_of_raw_binders = function
   | [] -> 0
@@ -103,8 +103,8 @@ let constant_entry_of_com (bl,com,comtypopt,opacity,boxed) =
   let env = Global.env() in
   match comtypopt with
       None -> 
-	let b = abstract_rawconstr com bl in
-	let j = judgment_of_rawconstr sigma env b in
+	let b = abstract_constr_expr com bl in
+	let j = interp_constr_judgment sigma env b in
 	{ const_entry_body = j.uj_val;
 	  const_entry_type = Some (refresh_universes j.uj_type);
           const_entry_opaque = opacity;
@@ -112,7 +112,7 @@ let constant_entry_of_com (bl,com,comtypopt,opacity,boxed) =
     | Some comtyp ->
 	(* We use a cast to avoid troubles with evars in comtyp *)
 	(* that can only be resolved knowing com *)
-	let b = abstract_rawconstr (mkCastC (com,DEFAULTcast,comtyp)) bl in
+	let b = abstract_constr_expr (mkCastC (com,DEFAULTcast,comtyp)) bl in
 	let (body,typ) = destSubCast (interp_constr sigma env b) in
 	{ const_entry_body = body;
 	  const_entry_type = Some typ;
@@ -190,7 +190,7 @@ let declare_one_assumption is_coe (local,kind) c (_,ident) =
   if is_coe then Class.try_add_new_coercion r local
 
 let declare_assumption idl is_coe k bl c =
-  let c = generalize_rawconstr c bl in
+  let c = generalize_constr_expr c bl in
   let c = interp_type Evd.empty (Global.env()) c in
   List.iter (declare_one_assumption is_coe k c) idl
 
@@ -279,26 +279,9 @@ let interp_mutual lparams lnamearconstrs finite =
       [] lnamearconstrs in
   if not (list_distinct allnames) then
     error "Two inductive objects have the same name";
-  let sigma = Evd.empty 
-  and env0 = Global.env() in
-  let env_params, params =
-    List.fold_left
-      (fun (env, params) d -> match d with
-	| LocalRawAssum ([_,na],(CHole _ as t)) ->
-	    let t = interp_binder sigma env na t in
-	    let d = (na,None,t) in
-	    (push_rel d env, d::params)
-	| LocalRawAssum (nal,t) ->
-	    let t = interp_type sigma env t in
-	    let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal in
-	    let ctx = List.rev ctx in
-	    (push_rel_context ctx env, ctx@params)
-	| LocalRawDef ((_,na),c) ->
-	    let c = judgment_of_rawconstr sigma env c in
-	    let d = (na, Some c.uj_val, c.uj_type) in
-	    (push_rel d env,d::params))
-      (env0,[]) lparams
-  in
+  let sigma = Evd.empty and env0 = Global.env() in
+  let env_params, params = interp_context sigma env0 lparams in
+
   (* Builds the params of the inductive entry *)
   let params' =
     List.map (fun (na,b,t) ->
@@ -364,8 +347,7 @@ let interp_mutual lparams lnamearconstrs finite =
          (* Interpret the constructor types *)
          let constrs =
 	   List.map 
-	     (interp_type_with_implicits sigma ind_env_params
-	       (paramassums,ind_impls))
+	     (interp_type sigma ind_env_params ~impls:(paramassums,ind_impls))
 	     bodies
 	 in
 
@@ -482,7 +464,7 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list)
   let (rec_sign,rec_impls,arityl) = 
     List.fold_left 
       (fun (env,impls,arl) ((recname,_,bl,arityc,_),_) -> 
-        let arityc = generalize_rawconstr arityc bl in
+        let arityc = generalize_constr_expr arityc bl in
         let arity = interp_type sigma env0 arityc in
 	let impl = 
 	  if Impargs.is_implicit_args()
@@ -506,9 +488,9 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list)
 	 Metasyntax.add_notation_interpretation df rec_impls c None) notations;
 	List.map2
 	  (fun ((_,_,bl,_,def),_) arity ->
-            let def = abstract_rawconstr def bl in
-            interp_casted_constr_with_implicits 
-	      sigma rec_sign rec_impls def arity)
+            let def = abstract_constr_expr def bl in
+            interp_casted_constr sigma rec_sign ~impls:([],rec_impls)
+              def arity)
           lnameargsardef arityl
       with e ->
 	States.unfreeze fs; raise e in
@@ -559,11 +541,10 @@ let build_corecursive lnameardef boxed =
     try 
       List.fold_left 
         (fun (env,arl) (recname,bl,arityc,_) -> 
-           let arityc = generalize_rawconstr arityc bl in
-           let arj = type_judgment_of_rawconstr Evd.empty env0 arityc in
-	   let arity = arj.utj_val in
+           let arityc = generalize_constr_expr arityc bl in
+           let arity = interp_type Evd.empty env0 arityc in
            let _ = declare_variable recname
-	     (Lib.cwd(),SectionLocalAssum arj.utj_val,IsAssumption Definitional) in
+	     (Lib.cwd(),SectionLocalAssum arity,IsAssumption Definitional) in
            (Environ.push_named (recname,None,arity) env, (arity::arl)))
         (env0,[]) lnameardef
     with e -> 
@@ -572,10 +553,10 @@ let build_corecursive lnameardef boxed =
   let recdef =
     try 
       List.map (fun (_,bl,arityc,def) ->
-        let arityc = generalize_rawconstr arityc bl in
-        let def = abstract_rawconstr def bl in
+        let arityc = generalize_constr_expr arityc bl in
+        let def = abstract_constr_expr def bl in
 	let arity = interp_constr sigma rec_sign arityc in
-                  interp_casted_constr sigma rec_sign def arity)
+        interp_casted_constr sigma rec_sign def arity)
         lnameardef
     with e -> 
       States.unfreeze fs; raise e 
@@ -656,7 +637,7 @@ let start_proof_com sopt kind (bl,t) hook =
  	  (Pfedit.get_all_proof_names ())
   in
   let env = Global.env () in
-  let c = interp_type Evd.empty env (generalize_rawconstr t bl) in
+  let c = interp_type Evd.empty env (generalize_constr_expr t bl) in
   let _ = Typeops.infer_type env c in
   start_proof id kind c hook
 
diff --git a/toplevel/command.mli b/toplevel/command.mli
index be815ffd66..be589da1a3 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -50,7 +50,7 @@ val build_corecursive : cofixpoint_expr list -> bool -> unit
 
 val build_scheme : (identifier located * bool * reference * rawsort) list -> unit
 
-val generalize_rawconstr : constr_expr -> local_binder list -> constr_expr
+val generalize_constr_expr : constr_expr -> local_binder list -> constr_expr
 
 val start_proof : identifier -> goal_kind -> constr ->
   declaration_hook -> unit
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 88bd4650c0..45f0632328 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -39,29 +39,12 @@ let interp_decl sigma env = function
 	| None -> c
 	| Some t -> mkCastC (c,DEFAULTcast,t)
       in
-      let j = judgment_of_rawconstr Evd.empty env c in
+      let j = interp_constr_judgment Evd.empty env c in
       (id,Some j.uj_val, j.uj_type)
 
 let typecheck_params_and_fields ps fs =
   let env0 = Global.env () in
-  let env1,newps =
-    List.fold_left
-      (fun (env,newps) d -> match d with
-	| LocalRawAssum ([_,na],(CHole _ as t)) ->
-	    let t = interp_binder Evd.empty env na t in
-	    let d = (na,None,t) in
-	    (push_rel d env, d::newps)
-	| LocalRawAssum (nal,t) ->
-	    let t = interp_type Evd.empty env t in
-	    let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal in
-	    let ctx = List.rev ctx in
-	    (push_rel_context ctx env, ctx@newps)
-	| LocalRawDef ((_,na),c) ->
-	    let c = judgment_of_rawconstr Evd.empty env c in
-	    let d = (na, Some c.uj_val, c.uj_type) in
-	    (push_rel d env, d::newps))
-      (env0,[]) ps
-  in
+  let env1,newps = interp_context Evd.empty env0 ps in
   let env2,newfs =
     List.fold_left
       (fun (env,newfs) d ->
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index 5f3cda588a..422b253437 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -670,11 +670,10 @@ let transf istype env iscast bl c =
   if Options.do_translate() then
     let r = 
       Constrintern.for_grammar
-        (Constrintern.interp_rawconstr_gen istype Evd.empty env false ([],[]))
-	c' in
+        (Constrintern.intern_gen istype Evd.empty env) c' in
     begin try
       (* Try to infer old case and type annotations *)
-      let _ = Pretyping.understand_gen_tcc Evd.empty env [] None r in 
+      let _ = Pretyping.understand_tcc Evd.empty env r in 
       (*msgerrnl (str "Typage OK");*) ()
     with e -> (*msgerrnl (str "Warning: can't type")*) () end;
     let c =
@@ -716,8 +715,7 @@ let transf_pattern env c =
   if Options.do_translate() then
     Constrextern.extern_rawconstr (Termops.vars_of_env env)
       (Constrintern.for_grammar
-	(Constrintern.interp_rawconstr_gen false Evd.empty env true ([],[]))
-	c)
+	(Constrintern.intern_gen false ~allow_soapp:true Evd.empty env) c)
   else c
 
 let pr_pattern c = pr lsimple (transf_pattern (Global.env()) c)
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 1e4b261036..bfe948c53f 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -660,7 +660,7 @@ let rec pr_vernac = function
 		in let ctx = List.rev ctx in
 		(Environ.push_rel_context ctx env, ctx@params)
 	    | LocalRawDef ((_,na),c) ->
-		let c = Constrintern.judgment_of_rawconstr sigma env c in
+		let c = Constrintern.interp_constr_judgment sigma env c in
 		let d = (na, Some c.Environ.uj_val, c.Environ.uj_type) in
 		(Environ.push_rel d env,d::params))
 	  (env0,[]) lparams in