Merge PR #946: Functional pretyping interface

11 files changed, 54 insertions, 112 deletions

diff --git a/API/API.mli b/API/API.mli
index e7a434634c..a90f8f84c7 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4017,18 +4017,11 @@ sig
       expand_evars : bool
     }
 
-  type pure_open_constr = Evd.evar_map * EConstr.constr
-  type glob_constr_ltac_closure = Glob_term.ltac_var_map * Glob_term.glob_constr
-
   val understand_ltac : inference_flags ->
                         Environ.env -> Evd.evar_map -> Glob_term.ltac_var_map ->
-                        typing_constraint -> Glob_term.glob_constr -> pure_open_constr
+                        typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.t
   val understand_tcc : ?flags:inference_flags -> Environ.env -> Evd.evar_map ->
                        ?expected_type:typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.constr
-  val type_uconstr :
-    ?flags:inference_flags ->
-    ?expected_type:typing_constraint ->
-    Geninterp.interp_sign -> Glob_term.closed_glob_constr -> EConstr.constr Tactypes.delayed_open
   val understand : ?flags:inference_flags -> ?expected_type:typing_constraint ->
                    Environ.env -> Evd.evar_map -> Glob_term.glob_constr -> Constr.t Evd.in_evar_universe_context
   val check_evars : Environ.env -> Evd.evar_map -> Evd.evar_map -> EConstr.constr -> unit
@@ -4387,8 +4380,10 @@ end
 
 module Evar_refiner :
 sig
+  type glob_constr_ltac_closure = Glob_term.ltac_var_map * Glob_term.glob_constr
+
   val w_refine : Evar.t * Evd.evar_info ->
-                 Pretyping.glob_constr_ltac_closure -> Evd.evar_map -> Evd.evar_map
+                 glob_constr_ltac_closure -> Evd.evar_map -> Evd.evar_map
 end
 
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index c9fc3aa4f3..e465677cde 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2038,7 +2038,9 @@ let interp_constr_evars_gen_impls env evdref
     ?(impls=empty_internalization_env) expected_type c =
   let c = intern_gen expected_type ~impls env c in
   let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:(expected_type == IsType) c in
-    understand_tcc_evars env evdref ~expected_type c, imps
+  let evd, c = understand_tcc env !evdref ~expected_type c in
+  evdref := evd;
+  c, imps
 
 let interp_constr_evars_impls env evdref ?(impls=empty_internalization_env) c =
   interp_constr_evars_gen_impls env evdref ~impls WithoutTypeConstraint c
@@ -2053,7 +2055,9 @@ let interp_type_evars_impls env evdref ?(impls=empty_internalization_env) c =
 
 let interp_constr_evars_gen env evdref ?(impls=empty_internalization_env) expected_type c =
   let c = intern_gen expected_type ~impls env c in
-  understand_tcc_evars env evdref ~expected_type c
+  let evd, c = understand_tcc env !evdref ~expected_type c in
+  evdref := evd;
+  c
 
 let interp_constr_evars env evdref ?(impls=empty_internalization_env) c =
   interp_constr_evars_gen env evdref WithoutTypeConstraint ~impls c
@@ -2098,7 +2102,9 @@ let interp_binder env sigma na t =
 let interp_binder_evars env evdref na t =
   let t = intern_gen IsType env t in
   let t' = locate_if_hole ?loc:(loc_of_glob_constr t) na t in
-  understand_tcc_evars env evdref ~expected_type:IsType t'
+  let evd, c = understand_tcc env !evdref ~expected_type:IsType t' in
+  evdref := evd;
+  c
 
 let my_intern_constr env lvar acc c =
   internalize env acc false lvar c
@@ -2125,7 +2131,8 @@ let interp_glob_context_evars env evdref k bl =
 	 if Option.is_empty b then locate_if_hole ?loc:(loc_of_glob_constr t) na t
 	 else t
        in
-       let t = understand_tcc_evars env evdref ~expected_type:IsType t' in
+       let (evd,t) = understand_tcc env !evdref ~expected_type:IsType t' in
+       evdref := evd;
 	match b with
 	    None ->
 	      let d = LocalAssum (na,t) in
@@ -2137,7 +2144,8 @@ let interp_glob_context_evars env evdref k bl =
 	      in
 		(push_rel d env, d::params, succ n, impls)
 	  | Some b ->
-	      let c = understand_tcc_evars env evdref ~expected_type:(OfType t) b in
+	      let (evd,c) = understand_tcc env !evdref ~expected_type:(OfType t) b in
+              evdref := evd;
 	      let d = LocalDef (na, c, t) in
 		(push_rel d env, d::params, n, impls))
       (env,[],k+1,[]) (List.rev bl)
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index f3f2f27e9e..b847aadf21 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -40,7 +40,7 @@ let with_delayed_uconstr ist c tac =
     fail_evar = false;
     expand_evars = true
   } in
-  let c = Pretyping.type_uconstr ~flags ist c in
+  let c = Tacinterp.type_uconstr ~flags ist c in
   Tacticals.New.tclDELAYEDWITHHOLES false c tac
 
 let replace_in_clause_maybe_by ist c1 c2 cl tac =
@@ -359,7 +359,7 @@ let refine_tac ist simple with_classes c =
     let flags =
       { constr_flags () with Pretyping.use_typeclasses = with_classes } in
     let expected_type = Pretyping.OfType concl in
-    let c = Pretyping.type_uconstr ~flags ~expected_type ist c in
+    let c = Tacinterp.type_uconstr ~flags ~expected_type ist c in
     let update = begin fun sigma ->
       c env sigma
     end in
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index 301943a509..5baa0d5c1d 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -48,7 +48,7 @@ let eval_uconstrs ist cs =
     expand_evars = true
   } in
   let map c env sigma = c env sigma in
-  List.map (fun c -> map (Pretyping.type_uconstr ~flags ist c)) cs
+  List.map (fun c -> map (Tacinterp.type_uconstr ~flags ist c)) cs
 
 let pr_auto_using_raw _ _ _  = Pptactic.pr_auto_using Ppconstr.pr_constr_expr
 let pr_auto_using_glob _ _ _ = Pptactic.pr_auto_using (fun (c,_) -> Printer.pr_glob_constr c)
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index d3e625e73a..51eed2f4ec 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1108,6 +1108,20 @@ let rec read_match_rule lfun ist env sigma = function
       :: read_match_rule lfun ist env sigma tl
   | [] -> []
 
+(* Fully evaluate an untyped constr *)
+let type_uconstr ?(flags = {(constr_flags ()) with use_hook = None })
+  ?(expected_type = WithoutTypeConstraint) ist c =
+  begin fun env sigma ->
+  let { closure; term } = c in
+  let vars = {
+    ltac_constrs = closure.typed;
+    ltac_uconstrs = closure.untyped;
+    ltac_idents = closure.idents;
+    ltac_genargs = Id.Map.empty;
+  } in
+  understand_ltac flags env sigma vars expected_type term
+  end
+
 let warn_deprecated_info =
   CWarnings.create ~name:"deprecated-info-tactical" ~category:"deprecated"
          (fun () ->
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index 73e4f3d6ab..c1ab2b4c49 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -54,6 +54,11 @@ val set_debug : debug_info -> unit
 (** Gives the state of debug *)
 val get_debug : unit -> debug_info
 
+val type_uconstr :
+  ?flags:Pretyping.inference_flags ->
+  ?expected_type:Pretyping.typing_constraint ->
+  Geninterp.interp_sign -> Glob_term.closed_glob_constr -> constr Tactypes.delayed_open
+
 (** Adds an interpretation function for extra generic arguments *)
 
 val interp_genarg : interp_sign -> glob_generic_argument -> Value.t Ftactic.t
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index b4d87dfdb0..40b8bcad92 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -47,8 +47,6 @@ open Misctypes
 module NamedDecl = Context.Named.Declaration
 
 type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
-type glob_constr_ltac_closure = ltac_var_map * glob_constr
-type pure_open_constr = evar_map * EConstr.constr
 
 (************************************************************************)
 (* This concerns Cases *)
@@ -385,9 +383,6 @@ let adjust_evar_source evdref na c =
      end
   | _, _ -> c
 
-(* Allow references to syntactically nonexistent variables (i.e., if applied on an inductive) *)
-let allow_anonymous_refs = ref false
-
 (* coerce to tycon if any *)
 let inh_conv_coerce_to_tycon ?loc resolve_tc env evdref j = function
   | None -> j
@@ -918,9 +913,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
       (* Make dependencies from arity signature impossible *)
     let arsgn =
       let arsgn,_ = get_arity env.ExtraEnv.env indf in
-	if not !allow_anonymous_refs then
-	  List.map (set_name Anonymous) arsgn
-	else arsgn
+      List.map (set_name Anonymous) arsgn
     in
       let indt = build_dependent_inductive env.ExtraEnv.env indf in
       let psign = LocalAssum (na, indt) :: arsgn in (* For locating names in [po] *)
@@ -981,10 +974,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 
       let arsgn =
 	let arsgn,_ = get_arity env.ExtraEnv.env indf in
-	  if not !allow_anonymous_refs then
-	      (* Make dependencies from arity signature impossible *)
-	    List.map (set_name Anonymous) arsgn
-	  else arsgn
+        (* Make dependencies from arity signature impossible *)
+        List.map (set_name Anonymous) arsgn
       in
       let nar = List.length arsgn in
       let indt = build_dependent_inductive env.ExtraEnv.env indf in
@@ -1018,13 +1009,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	let pi = beta_applist !evdref (pi, [EConstr.of_constr (build_dependent_constructor cs)]) in
         let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cs.cs_args in
 	let csgn =
-	  if not !allow_anonymous_refs then
-	    List.map (set_name Anonymous) cs_args
-	  else
-	    List.map (map_name (function Name _ as n -> n
-				       | Anonymous -> Name Namegen.default_non_dependent_ident))
-		     cs_args
-	in
+          List.map (set_name Anonymous) cs_args
+        in
 	let env_c = push_rel_context !evdref csgn env in
 	let bj = pretype (mk_tycon pi) env_c evdref lvar b in
 	  it_mkLambda_or_LetIn bj.uj_val cs_args in
@@ -1191,29 +1177,6 @@ let no_classes_no_fail_inference_flags = {
 let all_and_fail_flags = default_inference_flags true
 let all_no_fail_flags = default_inference_flags false
 
-let on_judgment sigma f j =
-  let c = mkCast(j.uj_val,DEFAULTcast, j.uj_type) in
-  let (c,_,t) = destCast sigma (f c) in
-  {uj_val = c; uj_type = t}
-
-let understand_judgment env sigma c =
-  let env = make_env env sigma in
-  let evdref = ref sigma in
-  let k0 = Context.Rel.length (rel_context env) in
-  let j = pretype k0 true empty_tycon env evdref empty_lvar c in
-  let j = on_judgment sigma (fun c ->
-    let evd, c = process_inference_flags all_and_fail_flags env.ExtraEnv.env sigma (!evdref,c) in 
-      evdref := evd; c) j
-  in j, Evd.evar_universe_context !evdref
-
-let understand_judgment_tcc env evdref c =
-  let env = make_env env !evdref in
-  let k0 = Context.Rel.length (rel_context env) in
-  let j = pretype k0 true empty_tycon env evdref empty_lvar c in
-  on_judgment !evdref (fun c ->
-    let (evd,c) = process_inference_flags all_no_fail_flags env.ExtraEnv.env Evd.empty (!evdref,c) in
-    evdref := evd; c) j
-
 let ise_pretype_gen_ctx flags env sigma lvar kind c =
   let evd, c = ise_pretype_gen flags env sigma lvar kind c in
   let evd, f = Evarutil.nf_evars_and_universes evd in
@@ -1231,36 +1194,10 @@ let understand_tcc ?(flags=all_no_fail_flags) env sigma ?(expected_type=WithoutT
   let (sigma, c) = ise_pretype_gen flags env sigma empty_lvar expected_type c in
   (sigma, c)
 
-let understand_tcc_evars ?(flags=all_no_fail_flags) env evdref ?(expected_type=WithoutTypeConstraint) c =
-  let sigma, c = ise_pretype_gen flags env !evdref empty_lvar expected_type c in
-  evdref := sigma;
-  c
-
 let understand_ltac flags env sigma lvar kind c =
   let (sigma, c) = ise_pretype_gen flags env sigma lvar kind c in
   (sigma, c)
 
-let constr_flags = {
-  use_typeclasses = true;
-  solve_unification_constraints = true;
-  use_hook = None;
-  fail_evar = true;
-  expand_evars = true }
-
-(* Fully evaluate an untyped constr *)
-let type_uconstr ?(flags = constr_flags)
-  ?(expected_type = WithoutTypeConstraint) ist c =
-  begin fun env sigma ->
-  let { closure; term } = c in
-  let vars = {
-    ltac_constrs = closure.typed;
-    ltac_uconstrs = closure.untyped;
-    ltac_idents = closure.idents;
-    ltac_genargs = Id.Map.empty;
-  } in
-  understand_ltac flags env sigma vars expected_type term
-  end
-
 let pretype k0 resolve_tc typcon env evdref lvar t =
   pretype k0 resolve_tc typcon (make_env env !evdref) evdref lvar t
 
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 6e533f1784..7395e94a09 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -27,9 +27,6 @@ val search_guard :
 
 type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
 
-type glob_constr_ltac_closure = ltac_var_map * glob_constr
-type pure_open_constr = evar_map * constr
-
 type inference_hook = env -> evar_map -> evar -> evar_map * constr
 
 type inference_flags = {
@@ -48,9 +45,6 @@ val all_no_fail_flags : inference_flags
 
 val all_and_fail_flags : inference_flags
 
-(** Allow references to syntactically nonexistent variables (i.e., if applied on an inductive) *)
-val allow_anonymous_refs : bool ref
-  
 (** Generic calls to the interpreter from glob_constr to open_constr;
     by default, inference_flags tell to use type classes and
     heuristics (but no external tactic solver hooks), as well as to
@@ -61,9 +55,6 @@ val allow_anonymous_refs : bool ref
 val understand_tcc : ?flags:inference_flags -> env -> evar_map ->
   ?expected_type:typing_constraint -> glob_constr -> evar_map * constr
 
-val understand_tcc_evars : ?flags:inference_flags -> env -> evar_map ref ->
-  ?expected_type:typing_constraint -> glob_constr -> constr
-
 (** More general entry point with evars from ltac *)
 
 (** Generic call to the interpreter from glob_constr to constr
@@ -78,7 +69,7 @@ val understand_tcc_evars : ?flags:inference_flags -> env -> evar_map ref ->
 
 val understand_ltac : inference_flags ->
   env -> evar_map -> ltac_var_map ->
-  typing_constraint -> glob_constr -> pure_open_constr
+  typing_constraint -> glob_constr -> evar_map * EConstr.t
 
 (** Standard call to get a constr from a glob_constr, resolving
     implicit arguments and coercions, and compiling pattern-matching;
@@ -90,20 +81,6 @@ val understand_ltac : inference_flags ->
 val understand : ?flags:inference_flags -> ?expected_type:typing_constraint ->
   env -> evar_map -> glob_constr -> Constr.constr Evd.in_evar_universe_context
 
-(** Idem but returns the judgment of the understood term *)
-
-val understand_judgment : env -> evar_map -> 
-  glob_constr -> unsafe_judgment Evd.in_evar_universe_context
-
-(** Idem but do not fail on unresolved evars (type cl*)
-val understand_judgment_tcc : env -> evar_map ref ->
-  glob_constr -> unsafe_judgment
-
-val type_uconstr :
-  ?flags:inference_flags ->
-  ?expected_type:typing_constraint ->
-  Geninterp.interp_sign -> Glob_term.closed_glob_constr -> constr Tactypes.delayed_open
-
 (** Trying to solve remaining evars and remaining conversion problems
     possibly using type classes, heuristics, external tactic solver
     hook depending on given flags. *)
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index cc81adb853..48fa2202ee 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -13,11 +13,14 @@ open Evd
 open Evarutil
 open Evarsolve
 open Pp
+open Glob_term
 
 (******************************************)
 (* Instantiation of existential variables *)
 (******************************************)
 
+type glob_constr_ltac_closure = ltac_var_map * glob_constr
+
 let depends_on_evar sigma evk _ (pbty,_,t1,t2) =
   let t1 = EConstr.of_constr t1 in
   let t2 = EConstr.of_constr t2 in
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index b65ffb1bee..5d69715967 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -7,9 +7,11 @@
 (************************************************************************)
 
 open Evd
-open Pretyping
+open Glob_term
 
 (** Refinement of existential variables. *)
 
+type glob_constr_ltac_closure = ltac_var_map * glob_constr
+
 val w_refine : evar * evar_info ->
   glob_constr_ltac_closure -> evar_map -> evar_map
diff --git a/vernac/command.ml b/vernac/command.ml
index e04bebe33b..a315ac14e2 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -393,8 +393,9 @@ let is_impredicative env u =
 
 let interp_ind_arity env evdref ind =
   let c = intern_gen IsType env ind.ind_arity in
-  let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:true c in
-  let t, impls = understand_tcc_evars env evdref ~expected_type:IsType c, imps in
+  let impls = Implicit_quantifiers.implicits_of_glob_constr ~with_products:true c in
+  let (evd,t) = understand_tcc env !evdref ~expected_type:IsType c in
+  evdref := evd;
   let pseudo_poly = check_anonymous_type c in
   let () = if not (Reductionops.is_arity env !evdref t) then
     user_err ?loc:(constr_loc ind.ind_arity) (str "Not an arity")