Imported Upstream version 8.4~betaupstream/8.4_beta

1 files changed, 159 insertions, 141 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index a3b1dd18..901936f3 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1,13 +1,27 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pretyping.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* This file contains the syntax-directed part of the type inference
+   algorithm introduced by Murthy in Coq V5.10, 1995; the type
+   inference algorithm was initially developed in a file named trad.ml
+   which formerly contained a simple concrete-to-abstract syntax
+   translation function introduced in CoC V4.10 for implementing the
+   "exact" tactic, 1989 *)
+(* Support for typing term in Ltac environment by David Delahaye, 2000 *)
+(* Type inference algorithm made a functor of the coercion and
+   pattern-matching compilation by Matthieu Sozeau, March 2006 *)
+(* Fixpoint guard index computation by Pierre Letouzey, July 2007 *)
 
+(* Structural maintainer: Hugo Herbelin *)
+(* Secondary maintenance: collective *)
+
+
+open Compat
 open Pp
 open Util
 open Names
@@ -26,7 +40,7 @@ open List
 open Recordops
 open Evarutil
 open Pretype_errors
-open Rawterm
+open Glob_term
 open Evarconv
 open Pattern
 
@@ -34,7 +48,8 @@ type typing_constraint = OfType of types option | IsType
 type var_map = (identifier * constr_under_binders) list
 type unbound_ltac_var_map = (identifier * identifier option) list
 type ltac_var_map = var_map * unbound_ltac_var_map
-type rawconstr_ltac_closure = ltac_var_map * rawconstr
+type glob_constr_ltac_closure = ltac_var_map * glob_constr
+type pure_open_constr = evar_map * constr
 
 (************************************************************************)
 (* This concerns Cases *)
@@ -55,7 +70,7 @@ let search_guard loc env possible_indexes fixdefs =
     let indexes = Array.of_list (List.map List.hd possible_indexes) in
     let fix = ((indexes, 0),fixdefs) in
     (try check_fix env fix with
-       | e -> if loc = dummy_loc then raise e else Stdpp.raise_with_loc loc e);
+       | e -> if loc = dummy_loc then raise e else Loc.raise loc e);
     indexes
   else
     (* we now search recursively amoungst all combinations *)
@@ -72,20 +87,53 @@ let search_guard loc env possible_indexes fixdefs =
 	 user_err_loc (loc,"search_guard", Pp.str errmsg)
      with Found indexes -> indexes)
 
-(* To embed constr in rawconstr *)
+(* To embed constr in glob_constr *)
 let ((constr_in : constr -> Dyn.t),
      (constr_out : Dyn.t -> constr)) = Dyn.create "constr"
 
 (** Miscellaneous interpretation functions *)
 
 let interp_sort = function
-  | RProp c -> Prop c
-  | RType _ -> new_Type_sort ()
+  | GProp c -> Prop c
+  | GType _ -> new_Type_sort ()
 
 let interp_elimination_sort = function
-  | RProp Null -> InProp
-  | RProp Pos  -> InSet
-  | RType _ -> InType
+  | GProp Null -> InProp
+  | GProp Pos  -> InSet
+  | GType _ -> InType
+
+let resolve_evars env evdref fail_evar resolve_classes =
+  if resolve_classes then
+    evdref := (Typeclasses.resolve_typeclasses ~onlyargs:false
+		 ~split:true ~fail:fail_evar env !evdref);
+  (* Resolve eagerly, potentially making wrong choices *)
+  evdref := (try consider_remaining_unif_problems
+	       ~ts:(Typeclasses.classes_transparent_state ()) env !evdref
+	     with e -> if fail_evar then raise e else !evdref)
+
+let solve_remaining_evars fail_evar use_classes hook env initial_sigma (evd,c) =
+  let evdref = ref evd in
+  resolve_evars env evdref fail_evar use_classes;
+  let rec proc_rec c =
+    let c = Reductionops.whd_evar !evdref c in
+    match kind_of_term c with
+    | Evar (evk,args as ev) when not (Evd.mem initial_sigma evk) ->
+        let sigma = !evdref in
+	(try
+	   let c = hook env sigma ev in
+	   evdref := Evd.define evk c !evdref;
+	   c
+	 with Exit ->
+           if fail_evar then
+	     let evi = Evd.find_undefined sigma evk in
+             let (loc,src) = evar_source evk !evdref in
+	     Pretype_errors.error_unsolvable_implicit loc env sigma evi src None
+           else
+             c)
+    | _ -> map_constr proc_rec c in
+  let c = proc_rec c in
+  (* Side-effect *)
+  !evdref,c
 
 module type S =
 sig
@@ -95,20 +143,20 @@ sig
   (* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
   val allow_anonymous_refs : bool ref
 
-  (* Generic call to the interpreter from rawconstr to open_constr, leaving
+  (* Generic call to the interpreter from glob_constr 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 : ?resolve_classes:bool ->
-    evar_map -> env -> ?expected_type:types -> rawconstr -> open_constr
+    evar_map -> env -> ?expected_type:types -> glob_constr -> open_constr
 
   val understand_tcc_evars : ?fail_evar:bool -> ?resolve_classes:bool ->
-    evar_map ref -> env -> typing_constraint -> rawconstr -> constr
+    evar_map ref -> env -> typing_constraint -> glob_constr -> constr
 
   (* More general entry point with evars from ltac *)
 
-  (* Generic call to the interpreter from rawconstr to constr, failing
-     unresolved holes in the rawterm cannot be instantiated.
+  (* Generic call to the interpreter from glob_constr to constr, failing
+     unresolved holes in the glob_constr cannot be instantiated.
 
      In [understand_ltac expand_evars sigma env ltac_env constraint c],
 
@@ -120,29 +168,29 @@ sig
 
   val understand_ltac :
     bool -> evar_map -> env -> ltac_var_map ->
-    typing_constraint -> rawconstr -> evar_map * constr
+    typing_constraint -> glob_constr -> pure_open_constr
 
-  (* Standard call to get a constr from a rawconstr, resolving implicit args *)
+  (* Standard call to get a constr from a glob_constr, resolving implicit args *)
 
   val understand : evar_map -> env -> ?expected_type:Term.types ->
-    rawconstr -> constr
+    glob_constr -> constr
 
-  (* Idem but the rawconstr is intended to be a type *)
+  (* Idem but the glob_constr is intended to be a type *)
 
-  val understand_type : evar_map -> env -> rawconstr -> constr
+  val understand_type : evar_map -> env -> glob_constr -> constr
 
   (* A generalization of the two previous case *)
 
   val understand_gen : typing_constraint -> evar_map -> env ->
-    rawconstr -> constr
+    glob_constr -> constr
 
   (* Idem but returns the judgment of the understood term *)
 
-  val understand_judgment : evar_map -> env -> rawconstr -> unsafe_judgment
+  val understand_judgment : evar_map -> env -> glob_constr -> unsafe_judgment
 
   (* Idem but do not fail on unresolved evars *)
 
-  val understand_judgment_tcc : evar_map ref -> env -> rawconstr -> unsafe_judgment
+  val understand_judgment_tcc : evar_map ref -> env -> glob_constr -> unsafe_judgment
 
   (*i*)
   (* Internal of Pretyping...
@@ -150,15 +198,15 @@ sig
    *)
   val pretype :
     type_constraint -> env -> evar_map ref ->
-    ltac_var_map -> rawconstr -> unsafe_judgment
+    ltac_var_map -> glob_constr -> unsafe_judgment
 
   val pretype_type :
     val_constraint -> env -> evar_map ref ->
-    ltac_var_map -> rawconstr -> unsafe_type_judgment
+    ltac_var_map -> glob_constr -> unsafe_type_judgment
 
   val pretype_gen :
     bool -> bool -> bool -> evar_map ref -> env ->
-    ltac_var_map -> typing_constraint -> rawconstr -> constr
+    ltac_var_map -> typing_constraint -> glob_constr -> constr
 
     (*i*)
 end
@@ -207,13 +255,6 @@ module Pretyping_F (Coercion : Coercion.S) = struct
               i lna vdefj lar
 	done
 
-  let check_branches_message loc env evdref c (explft,lft) =
-    for i = 0 to Array.length explft - 1 do
-      if not (e_cumul env evdref lft.(i) explft.(i)) then
-	let sigma = !evdref in
-	  error_ill_formed_branch_loc loc env sigma c i lft.(i) explft.(i)
-    done
-
   (* coerce to tycon if any *)
   let inh_conv_coerce_to_tycon loc env evdref j = function
     | None -> j
@@ -241,45 +282,33 @@ module Pretyping_F (Coercion : Coercion.S) = struct
       errorlabstrm "" (str "Cannot reinterpret " ++ quote (print_constr c) ++ str " in the current environment.")
 
   let pretype_id loc env sigma (lvar,unbndltacvars) id =
+    (* Look for the binder of [id] *)
     try
       let (n,_,typ) = lookup_rel_id id (rel_context env) in
       { uj_val  = mkRel n; uj_type = lift n typ }
     with Not_found ->
+    (* Check if [id] is an ltac variable *)
     try
       let (ids,c) = List.assoc id lvar in
       let subst = List.map (invert_ltac_bound_name env id) ids in
       let c = substl subst c in
       { uj_val = c; uj_type = protected_get_type_of env sigma c }
     with Not_found ->
+    (* Check if [id] is a section or goal variable *)
     try
       let (_,_,typ) = lookup_named id env in
       { uj_val  = mkVar id; uj_type = typ }
     with Not_found ->
-    try (* To build a nicer ltac error message *)
+    (* [id] not found, build nice error message if [id] yet known from ltac *)
+    try
       match List.assoc id unbndltacvars with
       | None -> user_err_loc (loc,"",
 	  str "Variable " ++ pr_id id ++ str " should be bound to a term.")
       | Some id0 -> Pretype_errors.error_var_not_found_loc loc id0
     with Not_found ->
+    (* [id] not found, standard error message *)
       error_var_not_found_loc loc id
 
-  (* make a dependent predicate from an undependent one *)
-
-  let make_dep_of_undep env (IndType (indf,realargs)) pj =
-    let n = List.length realargs in
-    let rec decomp n p =
-      if n=0 then p else
-	match kind_of_term p with
-	  | Lambda (_,_,c) -> decomp (n-1) c
-	  | _ -> decomp (n-1) (applist (lift 1 p, [mkRel 1]))
-    in
-    let sign,s = decompose_prod_n n pj.uj_type in
-    let ind = build_dependent_inductive env indf in
-    let s' = mkProd (Anonymous, ind, s) in
-    let ccl = lift 1 (decomp n pj.uj_val) in
-    let ccl' = mkLambda (Anonymous, ind, ccl) in
-      {uj_val=it_mkLambda ccl' sign; uj_type=it_mkProd s' sign}
-
   let evar_kind_of_term sigma c =
     kind_of_term (whd_evar sigma c)
 
@@ -290,27 +319,30 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     let c = constr_of_global ref in
       make_judge c (Retyping.get_type_of env Evd.empty c)
 
-  let pretype_sort = function
-    | RProp c -> judge_of_prop_contents c
-    | RType _ -> judge_of_new_Type ()
+  let pretype_sort evdref = function
+    | GProp c -> judge_of_prop_contents c
+    | GType _ -> evd_comb0 judge_of_new_Type evdref
 
   exception Found of fixpoint
 
+  let new_type_evar evdref env loc =
+    evd_comb0 (fun evd -> Evarutil.new_type_evar evd env ~src:(loc,InternalHole)) evdref
+
   (* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *)
   (* in environment [env], with existential variables [evdref] and *)
   (* the type constraint tycon *)
   let rec pretype (tycon : type_constraint) env evdref lvar = function
-    | RRef (loc,ref) ->
+    | GRef (loc,ref) ->
 	inh_conv_coerce_to_tycon loc env evdref
 	  (pretype_ref evdref env ref)
 	  tycon
 
-    | RVar (loc, id) ->
+    | GVar (loc, id) ->
 	inh_conv_coerce_to_tycon loc env evdref
 	  (pretype_id loc env !evdref lvar id)
 	  tycon
 
-    | REvar (loc, evk, instopt) ->
+    | GEvar (loc, evk, instopt) ->
 	(* Ne faudrait-il pas s'assurer que hyps est bien un
 	   sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *)
 	let hyps = evar_filtered_context (Evd.find !evdref evk) in
@@ -321,24 +353,23 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	let j = (Retyping.get_judgment_of env !evdref c) in
 	  inh_conv_coerce_to_tycon loc env evdref j tycon
 
-    | RPatVar (loc,(someta,n)) ->
+    | GPatVar (loc,(someta,n)) ->
 	let ty =
           match tycon with
             | Some (None, ty) -> ty
-            | None | Some _ ->
-		e_new_evar evdref env ~src:(loc,InternalHole) (new_Type ()) in
+            | None | Some _ -> new_type_evar evdref env loc in
         let k = MatchingVar (someta,n) in
 	{ uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty }
 
-    | RHole (loc,k) ->
+    | GHole (loc,k) ->
 	let ty =
           match tycon with
             | Some (None, ty) -> ty
             | None | Some _ ->
-		e_new_evar evdref env ~src:(loc,InternalHole) (new_Type ()) in
+		new_type_evar evdref env loc in
 	  { uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty }
 
-    | RRec (loc,fixkind,names,bl,lar,vdef) ->
+    | GRec (loc,fixkind,names,bl,lar,vdef) ->
 	let rec type_bl env ctxt = function
             [] -> ctxt
           | (na,bk,None,ty)::bl ->
@@ -379,7 +410,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	let ftys = Array.map (nf_evar !evdref) ftys in
 	let fdefs = Array.map (fun x -> nf_evar !evdref (j_val x)) vdefj in
  	let fixj = match fixkind with
-	  | RFix (vn,i) ->
+	  | GFix (vn,i) ->
 	      (* First, let's find the guard indexes. *)
 	      (* If recursive argument was not given by user, we try all args.
 	         An earlier approach was to look only for inductive arguments,
@@ -395,22 +426,23 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	      let fixdecls = (names,ftys,fdefs) in
 	      let indexes = search_guard loc env possible_indexes fixdecls in
 	      make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
-	  | RCoFix i ->
+	  | GCoFix i ->
 	      let cofix = (i,(names,ftys,fdefs)) in
-	      (try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e);
+	      (try check_cofix env cofix with e -> Loc.raise loc e);
 	      make_judge (mkCoFix cofix) ftys.(i) in
 	inh_conv_coerce_to_tycon loc env evdref fixj tycon
 
-    | RSort (loc,s) ->
-	inh_conv_coerce_to_tycon loc env evdref (pretype_sort s) tycon
+    | GSort (loc,s) ->
+	let j = pretype_sort evdref s in
+	  inh_conv_coerce_to_tycon loc env evdref j tycon
 
-    | RApp (loc,f,args) ->
+    | GApp (loc,f,args) ->
 	let fj = pretype empty_tycon env evdref lvar f in
- 	let floc = loc_of_rawconstr f in
+ 	let floc = loc_of_glob_constr f in
 	let rec apply_rec env n resj = function
 	  | [] -> resj
 	  | c::rest ->
-	      let argloc = loc_of_rawconstr c in
+	      let argloc = loc_of_glob_constr c in
 	      let resj = evd_comb1 (Coercion.inh_app_fun env) evdref resj in
               let resty = whd_betadeltaiota env !evdref resj.uj_type in
       		match kind_of_term resty with
@@ -444,7 +476,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  | _ -> resj in
 	inh_conv_coerce_to_tycon loc env evdref resj tycon
 
-    | RLambda(loc,name,bk,c1,c2)      ->
+    | GLambda(loc,name,bk,c1,c2)      ->
 	let (name',dom,rng) = evd_comb1 (split_tycon loc env) evdref tycon in
 	let dom_valcon = valcon_of_tycon dom in
 	let j = pretype_type dom_valcon env evdref lvar c1 in
@@ -452,7 +484,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	let j' = pretype rng (push_rel var env) evdref lvar c2 in
 	  judge_of_abstraction env (orelse_name name name') j j'
 
-    | RProd(loc,name,bk,c1,c2)        ->
+    | GProd(loc,name,bk,c1,c2)        ->
 	let j = pretype_type empty_valcon env evdref lvar c1 in
 	let j' =
 	  if name = Anonymous then
@@ -465,13 +497,13 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	in
 	let resj =
 	  try judge_of_product env name j j'
-	  with TypeError _ as e -> Stdpp.raise_with_loc loc e in
+	  with TypeError _ as e -> Loc.raise loc e in
 	  inh_conv_coerce_to_tycon loc env evdref resj tycon
 
-    | RLetIn(loc,name,c1,c2)      ->
+    | GLetIn(loc,name,c1,c2)      ->
 	let j =
 	  match c1 with
-	  | RCast (loc, c, CastConv (DEFAULTcast, t)) ->
+	  | GCast (loc, c, CastConv (DEFAULTcast, t)) ->
 	      let tj = pretype_type empty_valcon env evdref lvar t in
 		pretype (mk_tycon tj.utj_val) env evdref lvar c
 	  | _ -> pretype empty_tycon env evdref lvar c1
@@ -483,12 +515,12 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ;
 	    uj_type = subst1 j.uj_val j'.uj_type }
 
-    | RLetTuple (loc,nal,(na,po),c,d) ->
+    | GLetTuple (loc,nal,(na,po),c,d) ->
 	let cj = pretype empty_tycon env evdref lvar c in
 	let (IndType (indf,realargs)) =
 	  try find_rectype env !evdref cj.uj_type
 	  with Not_found ->
-	    let cloc = loc_of_rawconstr c in
+	    let cloc = loc_of_glob_constr c in
 	      error_case_not_inductive_loc cloc env !evdref cj
 	in
 	let cstrs = get_constructors env indf in
@@ -524,10 +556,11 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		     let fj = pretype (mk_tycon fty) env_f evdref lvar d in
 		     let f = it_mkLambda_or_LetIn fj.uj_val fsign in
 		     let v =
-		       let mis,_ = dest_ind_family indf in
-		       let ci = make_case_info env mis LetStyle in
-			 mkCase (ci, p, cj.uj_val,[|f|]) in
-		       { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl }
+		       let ind,_ = dest_ind_family indf in
+		       let ci = make_case_info env ind LetStyle in
+		       Typing.check_allowed_sort env !evdref ind cj.uj_val p;
+		       mkCase (ci, p, cj.uj_val,[|f|]) in
+		     { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl }
 
 		 | None ->
 		     let tycon = lift_tycon cs.cs_nargs tycon in
@@ -543,18 +576,18 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		     let ccl = refresh_universes ccl in
 		     let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
 		     let v =
-		       let mis,_ = dest_ind_family indf in
-		       let ci = make_case_info env mis LetStyle in
-			 mkCase (ci, p, cj.uj_val,[|f|] )
-		     in
-		       { uj_val = v; uj_type = ccl })
+		       let ind,_ = dest_ind_family indf in
+		       let ci = make_case_info env ind LetStyle in
+		       Typing.check_allowed_sort env !evdref ind cj.uj_val p;
+		       mkCase (ci, p, cj.uj_val,[|f|])
+		     in { uj_val = v; uj_type = ccl })
 
-    | RIf (loc,c,(na,po),b1,b2) ->
+    | GIf (loc,c,(na,po),b1,b2) ->
 	let cj = pretype empty_tycon env evdref lvar c in
 	let (IndType (indf,realargs)) =
 	  try find_rectype env !evdref cj.uj_type
 	  with Not_found ->
-	    let cloc = loc_of_rawconstr c in
+	    let cloc = loc_of_glob_constr c in
 	      error_case_not_inductive_loc cloc env !evdref cj in
 	let cstrs = get_constructors env indf in
 	  if Array.length cstrs <> 2 then
@@ -577,15 +610,11 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		let ccl = nf_evar !evdref pj.utj_val in
 		let pred = it_mkLambda_or_LetIn ccl psign in
 		let typ = lift (- nar) (beta_applist (pred,[cj.uj_val])) in
-		let jtyp = inh_conv_coerce_to_tycon loc env evdref {uj_val = pred;
-								     uj_type = typ} tycon
-		in
-		  jtyp.uj_val, jtyp.uj_type
+	        pred, typ
 	    | None ->
 		let p = match tycon with
 		  | Some (None, ty) -> ty
-		  | None | Some _ ->
-                      e_new_evar evdref env ~src:(loc,InternalHole) (new_Type ())
+		  | None | Some _ -> new_type_evar evdref env loc
 		in
 		  it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
 	  let pred = nf_evar !evdref pred in
@@ -611,18 +640,20 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  let b1 = f cstrs.(0) b1 in
 	  let b2 = f cstrs.(1) b2 in
 	  let v =
-	    let mis,_ = dest_ind_family indf in
-	    let ci = make_case_info env mis IfStyle in
-	      mkCase (ci, pred, cj.uj_val, [|b1;b2|])
+	    let ind,_ = dest_ind_family indf in
+	    let ci = make_case_info env ind IfStyle in
+	    let pred = nf_evar !evdref pred in
+	    Typing.check_allowed_sort env !evdref ind cj.uj_val pred;
+	    mkCase (ci, pred, cj.uj_val, [|b1;b2|])
 	  in
 	    { uj_val = v; uj_type = p }
 
-    | RCases (loc,sty,po,tml,eqns) ->
+    | GCases (loc,sty,po,tml,eqns) ->
 	Cases.compile_cases loc sty
 	  ((fun vtyc env evdref -> pretype vtyc env evdref lvar),evdref)
 	  tycon env (* loc *) (po,tml,eqns)
 
-    | RCast (loc,c,k) ->
+    | GCast (loc,c,k) ->
 	let cj =
 	  match k with
 	      CastCoerce ->
@@ -633,29 +664,24 @@ module Pretyping_F (Coercion : Coercion.S) = struct
  		let cj = pretype empty_tycon env evdref lvar c in
 		let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in
 		let cj = match k with
-		  | VMcast when not (occur_existential cty || occur_existential tval) ->
-		     (try ignore (Reduction.vm_conv Reduction.CUMUL env cty tval); cj
-                      with Reduction.NotConvertible ->
-                        error_actual_type_loc loc env !evdref cj tval)
-
+		  | VMcast ->
+                      if not (occur_existential cty || occur_existential tval) then
+		      begin 
+			try 
+			  ignore (Reduction.vm_conv Reduction.CUMUL env cty tval); cj
+			with Reduction.NotConvertible -> 
+			  error_actual_type_loc loc env !evdref cj tval 
+		      end
+                      else user_err_loc (loc,"",str "Cannot check cast with vm: unresolved arguments remain.")
 		  | _ -> inh_conv_coerce_to_tycon loc env evdref cj (mk_tycon tval)
 		in
 		let v = mkCast (cj.uj_val, k, tval) in
 		  { uj_val = v; uj_type = tval }
 	in inh_conv_coerce_to_tycon loc env evdref cj tycon
 
-    | RDynamic (loc,d) ->
-	if (Dyn.tag d) = "constr" then
-	  let c = constr_out d in
-	  let j = (Retyping.get_judgment_of env !evdref c) in
-	    j
-	      (*inh_conv_coerce_to_tycon loc env evdref j tycon*)
-	else
-	  user_err_loc (loc,"pretype",(str "Not a constr tagged Dynamic."))
-
   (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *)
   and pretype_type valcon env evdref lvar = function
-    | RHole loc ->
+    | GHole loc ->
 	(match valcon with
 	   | Some v ->
                let s =
@@ -670,12 +696,12 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		 { utj_val = v;
 		   utj_type = s }
 	   | None ->
-	       let s = new_Type_sort () in
+	       let s = evd_comb0 new_sort_variable evdref in
 		 { utj_val = e_new_evar evdref env ~src:loc (mkSort s);
 		   utj_type = s})
     | c ->
 	let j = pretype empty_tycon env evdref lvar c in
-	let loc = loc_of_rawconstr c in
+	let loc = loc_of_glob_constr c in
 	let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) evdref j in
 	  match valcon with
 	    | None -> tj
@@ -683,7 +709,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		if e_cumul env evdref v tj.utj_val then tj
 		else
 		  error_unexpected_type_loc
-                    (loc_of_rawconstr c) env !evdref tj.utj_val v
+                    (loc_of_glob_constr c) env !evdref tj.utj_val v
 
   let pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c =
     let c' = match kind with
@@ -691,18 +717,12 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in
 	  (pretype tycon env evdref lvar c).uj_val
       | IsType ->
-	  (pretype_type empty_valcon env evdref lvar c).utj_val in
-    if resolve_classes then (
-      evdref := Typeclasses.resolve_typeclasses ~onlyargs:false
-	~split:true ~fail:fail_evar env !evdref);
-    evdref := (try consider_remaining_unif_problems env !evdref
-	       with e when not resolve_classes -> 
-		 consider_remaining_unif_problems env 
-		   (Typeclasses.resolve_typeclasses ~onlyargs:false
-		      ~split:true ~fail:fail_evar env !evdref));
-    let c = if expand_evar then nf_evar !evdref c' else c' in
-    if fail_evar then check_evars env Evd.empty !evdref c;
-    c
+	  (pretype_type empty_valcon env evdref lvar c).utj_val 
+    in
+      resolve_evars env evdref fail_evar resolve_classes;
+      let c = if expand_evar then nf_evar !evdref c' else c' in
+	if fail_evar then check_evars env Evd.empty !evdref c;
+	c
 
   (* TODO: comment faire remonter l'information si le typage a resolu des
      variables du sigma original. il faudrait que la fonction de typage
@@ -710,26 +730,24 @@ module Pretyping_F (Coercion : Coercion.S) = struct
   *)
 
   let understand_judgment sigma env c =
-    let evdref = ref (create_evar_defs sigma) in
+    let evdref = ref sigma in
     let j = pretype empty_tycon env evdref ([],[]) c in
-    let evd = consider_remaining_unif_problems env !evdref in
-    let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~split:false
-      ~fail:true env evd
-    in
-    let j = j_nf_evar evd j in
-    check_evars env sigma evd (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
-    j
+      resolve_evars env evdref true true;
+      let j = j_nf_evar !evdref j in
+	check_evars env sigma !evdref (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
+	j
 
   let understand_judgment_tcc evdref env c =
     let j = pretype empty_tycon env evdref ([],[]) c in
-    j_nf_evar !evdref j
+      resolve_evars env evdref false true;
+      j_nf_evar !evdref 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_pretype_gen expand_evar fail_evar resolve_classes sigma env lvar kind c =
-    let evdref = ref (Evd.create_evar_defs sigma) in
+    let evdref = ref sigma in
     let c = pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c in
     !evdref, c