Imported Upstream version 8.3.pl2upstream/8.3.pl2

6 files changed, 19 insertions, 15 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index bae89329..67bf7043 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: cases.ml 13728 2010-12-19 11:35:20Z herbelin $ *)
+(* $Id: cases.ml 13962 2011-04-06 17:00:45Z herbelin $ *)
 
 open Util
 open Names
@@ -1203,7 +1203,7 @@ and match_current pb tomatch =
 	  let case = mkCase (ci,nf_betaiota Evd.empty pred,current,brvals) in
 	  let inst = List.map mkRel deps in
 	  { uj_val = applist (case, inst);
-	    uj_type = substl inst typ }
+	    uj_type = prod_applist typ inst }
 
 and compile_branch current names deps pb arsign eqn cstr =
   let sign, pb = build_branch current deps names pb arsign eqn cstr in
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index a41cdd6f..b9fd307c 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: clenv.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
+(* $Id: clenv.ml 13902 2011-03-10 15:50:24Z msozeau $ *)
 
 open Pp
 open Util
@@ -305,7 +305,7 @@ let evar_clenv_unique_resolver = clenv_unique_resolver
 
 let connect_clenv gls clenv =
   { clenv with
-    evd = evars_reset_evd gls.sigma clenv.evd;
+    evd = evars_reset_evd ~with_conv_pbs:true gls.sigma clenv.evd;
     env = Global.env_of_context gls.it.evar_hyps }
 
 (* [clenv_fchain mv clenv clenv']
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 77442584..5d61e727 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evd.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
+(* $Id: evd.ml 13902 2011-03-10 15:50:24Z msozeau $ *)
 
 open Pp
 open Util
@@ -507,7 +507,9 @@ let empty =  {
   metas=Metamap.empty
 }
 
-let evars_reset_evd evd d = {d with evars = evd.evars}
+let evars_reset_evd ?(with_conv_pbs=false) evd d =
+  {d with evars = evd.evars; 
+     conv_pbs = if with_conv_pbs then evd.conv_pbs else d.conv_pbs}
 let add_conv_pb pb d = {d with conv_pbs = pb::d.conv_pbs}
 let evar_source evk d = (EvarMap.find d.evars evk).evar_source
 
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index ce4e1b28..c68cfffe 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: evd.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: evd.mli 13902 2011-03-10 15:50:24Z msozeau $ i*)
 
 (*i*)
 open Util
@@ -177,7 +177,7 @@ val existential_opt_value : evar_map -> existential -> constr option
 val subst_evar_defs_light : substitution -> evar_map -> evar_map
 
 (* spiwack: this function seems to somewhat break the abstraction. *)
-val evars_reset_evd  : evar_map ->  evar_map -> evar_map
+val evars_reset_evd  : ?with_conv_pbs:bool -> evar_map ->  evar_map -> evar_map
 
 
 (* spiwack: [is_undefined_evar] should be considered a candidate
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 1c17ff88..b8dc719b 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pretyping.ml 13408 2010-09-11 19:19:04Z herbelin $ *)
+(* $Id: pretyping.ml 13780 2011-01-07 16:37:57Z herbelin $ *)
 
 open Pp
 open Util
@@ -634,7 +634,10 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		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) ->
-		      ignore (Reduction.vm_conv Reduction.CUMUL env cty tval); cj
+		     (try ignore (Reduction.vm_conv Reduction.CUMUL env cty tval); cj
+                      with Reduction.NotConvertible ->
+                        error_actual_type_loc loc env !evdref cj tval)
+
 		  | _ -> inh_conv_coerce_to_tycon loc env evdref cj (mk_tycon tval)
 		in
 		let v = mkCast (cj.uj_val, k, tval) in
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 49ccb80c..68a67402 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tacred.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: tacred.ml 13804 2011-01-27 00:41:34Z letouzey $ *)
 
 open Pp
 open Util
@@ -216,8 +216,7 @@ let invert_name labs l na0 env sigma ref = function
 	  | EvalRel _ | EvalEvar _ -> None
 	  | EvalVar id' -> Some (EvalVar id)
 	  | EvalConst kn ->
-	      let (mp,dp,_) = repr_con kn in
-	      Some (EvalConst (make_con mp dp (label_of_id id))) in
+	      Some (EvalConst (con_with_label kn (label_of_id id))) in
 	match refi with
 	  | None -> None
 	  | Some ref ->
@@ -481,7 +480,6 @@ let reduce_mind_case_use_function func env sigma mia =
     | CoFix (bodynum,(names,_,_) as cofix) ->
 	let build_cofix_name =
 	  if isConst func then
-	    let (mp,dp,_) = repr_con (destConst func) in
             let minargs = List.length mia.mcargs in
 	    fun i ->
 	      if i = bodynum then Some (minargs,func)
@@ -492,7 +490,8 @@ let reduce_mind_case_use_function func env sigma mia =
 		       mutual inductive, try to reuse the global name if
 		       the block was indeed initially built as a global
 		       definition *)
-		    let kn = make_con mp dp (label_of_id id) in
+		    let kn = con_with_label (destConst func) (label_of_id id)
+		    in
 		    try match constant_opt_value env kn with
 		      | None -> None
                           (* TODO: check kn is correct *)