Imported Upstream version 8.4pl4dfsgupstream/8.4pl4dfsg

1 files changed, 24 insertions, 19 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 1dd71fab..08e8df05 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -200,11 +200,11 @@ sig
    * Unused outside, but useful for debugging
    *)
   val pretype :
-    type_constraint -> env -> evar_map ref ->
+    bool -> type_constraint -> env -> evar_map ref ->
     ltac_var_map -> glob_constr -> unsafe_judgment
 
   val pretype_type :
-    val_constraint -> env -> evar_map ref ->
+    bool -> val_constraint -> env -> evar_map ref ->
     ltac_var_map -> glob_constr -> unsafe_type_judgment
 
   val pretype_gen :
@@ -259,9 +259,9 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	done
 
   (* coerce to tycon if any *)
-  let inh_conv_coerce_to_tycon loc env evdref j = function
+  let inh_conv_coerce_to_tycon resolve_tc loc env evdref j = function
     | None -> j
-    | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) evdref j t
+    | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to resolve_tc loc env) evdref j t
 
   let push_rels vars env = List.fold_right push_rel vars env
 
@@ -297,18 +297,19 @@ module Pretyping_F (Coercion : Coercion.S) = struct
       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 ->
-    (* [id] not found, build nice error message if [id] yet known from ltac *)
+    (* if [id] an ltac variable not bound to a term *)
+    (* build a nice error message *)
     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 ->
+    (* 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 ->
     (* [id] not found, standard error message *)
       error_var_not_found_loc loc id
 
@@ -346,7 +347,11 @@ module Pretyping_F (Coercion : Coercion.S) = struct
   (* [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
+  let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t =
+    let pretype = pretype resolve_tc in
+    let pretype_type = pretype_type resolve_tc in
+    let inh_conv_coerce_to_tycon = inh_conv_coerce_to_tycon resolve_tc in
+    match t with
     | GRef (loc,ref) ->
 	inh_conv_coerce_to_tycon loc env evdref
 	  (pretype_ref loc evdref env ref)
@@ -459,7 +464,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  | [] -> resj
 	  | c::rest ->
 	      let argloc = loc_of_glob_constr c in
-	      let resj = evd_comb1 (Coercion.inh_app_fun env) evdref resj in
+	      let resj = evd_comb1 (Coercion.inh_app_fun resolve_tc env) evdref resj in
               let resty = whd_betadeltaiota env !evdref resj.uj_type in
       		match kind_of_term resty with
 		  | Prod (na,c1,c2) ->
@@ -696,7 +701,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	in inh_conv_coerce_to_tycon loc env evdref cj tycon
 
   (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *)
-  and pretype_type valcon env evdref lvar = function
+  and pretype_type resolve_tc valcon env evdref lvar = function
     | GHole loc ->
 	(match valcon with
 	   | Some v ->
@@ -716,7 +721,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		 { 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 j = pretype resolve_tc empty_tycon env evdref lvar 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
@@ -731,9 +736,9 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     let c' = match kind with
       | OfType exptyp ->
 	  let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in
-	  (pretype tycon env evdref lvar c).uj_val
+	  (pretype resolve_classes tycon env evdref lvar c).uj_val
       | IsType ->
-	  (pretype_type empty_valcon env evdref lvar c).utj_val 
+	  (pretype_type resolve_classes 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
@@ -747,14 +752,14 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 
   let understand_judgment sigma env c =
     let evdref = ref sigma in
-    let j = pretype empty_tycon env evdref ([],[]) c in
+    let j = pretype true empty_tycon env evdref ([],[]) c in
       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
+    let j = pretype true empty_tycon env evdref ([],[]) c in
       resolve_evars env evdref false true;
       j_nf_evar !evdref j