Imported Upstream version 8.3~rc1+dfsgupstream/8.3.rc1.dfsg

53 files changed, 182 insertions, 130 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index eb02f7ae..9027315e 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: cases.ml 13329 2010-07-26 11:05:39Z herbelin $ *)
 
 open Util
 open Names
@@ -1054,7 +1054,7 @@ let rec generalize_problem names pb = function
 	  tomatch = Abstract d :: tomatch;
           pred = generalize_predicate names i d pb.tomatch pb'.pred  }
 
-(* No more patterns: typing the right-hand-side of equations *)
+(* No more patterns: typing the right-hand side of equations *)
 let build_leaf pb =
   let rhs = extract_rhs pb in
   let j = pb.typing_function (mk_tycon pb.pred) rhs.rhs_env pb.evdref rhs.it in
@@ -1690,7 +1690,7 @@ let prepare_predicate loc typing_fun evdref env tomatchs sign tycon pred =
 
 let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, eqns) =
 
-  (* We build the matrix of patterns and right-hand-side *)
+  (* We build the matrix of patterns and right-hand side *)
   let matx = matx_of_eqns env tomatchl eqns in
 
   (* We build the vector of terms to match consistently with the *)
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 8b8ab3db..7bc635fb 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: cases.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Util
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index b5550c19..ec71159b 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: cbv.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Util
 open Pp
diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli
index c0081174..5486b064 100644
--- a/pretyping/cbv.mli
+++ b/pretyping/cbv.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: cbv.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 4079728c..17f18a9b 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: classops.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Util
 open Pp
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 54e57131..f905e392 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: classops.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 412763d7..a41cdd6f 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: clenv.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
 
 open Pp
 open Util
@@ -128,7 +128,7 @@ let clenv_conv_leq env sigma t c bound =
   let evd = Evd.create_goal_evar_defs sigma in
   let evars,args,_ = clenv_environments_evars env evd (Some bound) ty in
   let evars = Evarconv.the_conv_x_leq env t (applist (c,args)) evars in
-  let evars,_ = Evarconv.consider_remaining_unif_problems env evars in
+  let evars = Evarconv.consider_remaining_unif_problems env evars in
   let args = List.map (whd_evar evars) args in
   check_evars env sigma evars (applist (c,args));
   args
@@ -454,18 +454,23 @@ let clenv_constrain_dep_args hyps_only bl clenv =
 (****************************************************************)
 (* Clausal environment for an application *)
 
-let make_clenv_binding_gen hyps_only n gls (c,t) = function
+
+let make_clenv_binding_gen hyps_only n env sigma (c,t) = function
   | ImplicitBindings largs ->
-      let clause = mk_clenv_from_n gls n (c,t) in
+      let clause = mk_clenv_from_env env sigma n (c,t) in
       clenv_constrain_dep_args hyps_only largs clause
   | ExplicitBindings lbind ->
-      let clause = mk_clenv_rename_from_n gls n (c,t) in
-      clenv_match_args lbind clause
+      let clause = mk_clenv_from_env env sigma n 
+	(c,rename_bound_vars_as_displayed [] t) 
+      in clenv_match_args lbind clause
   | NoBindings ->
-      mk_clenv_from_n gls n (c,t)
+      mk_clenv_from_env env sigma n (c,t)
 
-let make_clenv_binding_apply gls n = make_clenv_binding_gen true n gls
-let make_clenv_binding = make_clenv_binding_gen false None
+let make_clenv_binding_env_apply env sigma n =
+  make_clenv_binding_gen true n env sigma
+	
+let make_clenv_binding_apply gls n = make_clenv_binding_gen true n (pf_env gls) gls.sigma
+let make_clenv_binding gls = make_clenv_binding_gen false None (pf_env gls) gls.sigma
 
 (****************************************************************)
 (* Pretty-print *)
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index aec9e7c9..b50e313c 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: clenv.mli 13332 2010-07-26 22:12:43Z msozeau $ i*)
 
 (*i*)
 open Util
@@ -111,6 +111,9 @@ val clenv_unify_meta_types : ?flags:unify_flags -> clausenv -> clausenv
 val make_clenv_binding_apply :
   evar_info sigma -> int option -> constr * constr -> constr bindings ->
    clausenv
+val make_clenv_binding_env_apply :
+  env -> evar_map -> int option -> constr * constr -> constr bindings ->
+   clausenv
 val make_clenv_binding :
   evar_info sigma -> constr * constr -> constr bindings -> clausenv
 
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 48a8d28e..dd099aa1 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -5,7 +5,7 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(* $Id$ *)
+(* $Id: coercion.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Util
 open Names
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index 89be8069..00848dac 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: coercion.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Util
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index c0e5234b..e435484e 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: detyping.ml 13329 2010-07-26 11:05:39Z herbelin $ *)
 
 open Pp
 open Util
@@ -364,6 +364,8 @@ let detype_sort = function
   | Prop c -> RProp c
   | Type u -> RType (Some u)
 
+type binder_kind = BProd | BLambda | BLetIn
+
 (**********************************************************************)
 (* Main detyping function                                             *)
 
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index ecf724ca..cdb840b6 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: detyping.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Util
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 20957e07..51183be3 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: evarconv.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
 
 open Pp
 open Util
@@ -551,10 +551,10 @@ let apply_conversion_problem_heuristic env evd pbty t1 t2 =
 let consider_remaining_unif_problems env evd =
   let (evd,pbs) = extract_all_conv_pbs evd in
   List.fold_left
-    (fun (evd,b as p) (pbty,env,t1,t2) ->
-      if b then apply_conversion_problem_heuristic env evd pbty t1 t2 else p)
-    (evd,true)
-    pbs
+    (fun evd (pbty,env,t1,t2) ->
+      let evd', b = apply_conversion_problem_heuristic env evd pbty t1 t2 in
+	if b then evd' else Pretype_errors.error_cannot_unify env evd (t1, t2))
+    evd pbs
 
 (* Main entry points *)
 
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index add7ccd4..b0702038 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: evarconv.mli 13332 2010-07-26 22:12:43Z msozeau $ i*)
 
 (*i*)
 open Term
@@ -34,7 +34,7 @@ val evar_eqappr_x :
       evar_map * bool
 (*i*)
 
-val consider_remaining_unif_problems : env -> evar_map -> evar_map * bool
+val consider_remaining_unif_problems : env -> evar_map -> evar_map
 
 val check_conv_record : constr * types list -> constr * types list ->
   constr * constr list * (constr list * constr list) *
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index ac653c75..09ec8dda 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: evarutil.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
 
 open Util
 open Pp
@@ -1434,6 +1434,10 @@ let judge_of_new_Type () = Typeops.judge_of_type (new_univ ())
    constraint on its domain and codomain. If the input constraint is
    an evar instantiate it with the product of 2 new evars. *)
 
+let unlift_tycon init cur c =
+  if cur = 1 then None, c
+  else Some (init, pred cur), c
+
 let split_tycon loc env evd tycon =
   let rec real_split evd c =
     let t = whd_betadeltaiota env evd c in
@@ -1453,14 +1457,7 @@ let split_tycon loc env evd tycon =
 		 let evd', (n, dom, rng) = real_split evd c in
 		   evd', (n, mk_tycon dom, mk_tycon rng)
 	     | Some (init, cur) ->
-		 if cur = 0 then
-		   let evd', (x, dom, rng) = real_split evd c in
-		     evd, (Anonymous,
-			  Some (None, dom),
-			  Some (None, rng))
-		 else
-		   evd, (Anonymous, None,
-			Some (if cur = 1 then None,c else Some (init, pred cur), c)))
+		 evd, (Anonymous, None, Some (unlift_tycon init cur c)))
 
 let valcon_of_tycon x =
   match x with
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index d0b65d54..d677b972 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: evarutil.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Util
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 109fea4a..77442584 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: evd.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
 
 open Pp
 open Util
@@ -498,7 +498,8 @@ let create_evar_defs sigma = { sigma with
   conv_pbs=[]; last_mods=ExistentialSet.empty; metas=Metamap.empty }
 (* spiwack: tentatively deprecated *)
 let create_goal_evar_defs sigma = { sigma with
-   conv_pbs=[]; last_mods=ExistentialSet.empty; metas=Metamap.empty }
+   (* conv_pbs=[]; last_mods=ExistentialSet.empty; metas=Metamap.empty } *)
+  metas=Metamap.empty } 
 let empty =  {
   evars=EvarMap.empty;
   conv_pbs=[];
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index ea484b5f..ce4e1b28 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: evd.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Util
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index f83aff69..927af594 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: indrec.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 (* File initially created by Christine Paulin, 1996 *)
 
diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli
index ea5d13dc..188ad74d 100644
--- a/pretyping/indrec.mli
+++ b/pretyping/indrec.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: indrec.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 03589c4f..85c865fa 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: inductiveops.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Util
 open Names
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 7f29cba9..251c6b2e 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: inductiveops.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 open Names
 open Term
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index 843122e7..6ee67bf2 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: matching.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 (*i*)
 open Util
diff --git a/pretyping/matching.mli b/pretyping/matching.mli
index 7677c076..25863129 100644
--- a/pretyping/matching.mli
+++ b/pretyping/matching.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: matching.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
index 3c95d1ea..6e3e2f7c 100644
--- a/pretyping/namegen.ml
+++ b/pretyping/namegen.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: namegen.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 (* Created from contents that was formerly in termops.ml and
    nameops.ml, Nov 2009 *)
diff --git a/pretyping/namegen.mli b/pretyping/namegen.mli
index fa89426c..419624b8 100644
--- a/pretyping/namegen.mli
+++ b/pretyping/namegen.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: namegen.mli 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Names
 open Term
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 4f62252f..d1c4cfc1 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: pattern.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Util
 open Names
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index 92344e47..fbc6bbaa 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: pattern.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Pp
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 9f441c21..6befdedc 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: pretype_errors.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Util
 open Stdpp
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index ad122127..496e16d2 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: pretype_errors.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Pp
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 5438d982..7b4b5e07 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: pretyping.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
 
 open Pp
 open Util
@@ -684,11 +684,14 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  (pretype tycon env evdref lvar c).uj_val
       | IsType ->
 	  (pretype_type empty_valcon env evdref lvar c).utj_val in
-    evdref := fst (consider_remaining_unif_problems env !evdref);
-    if resolve_classes then
-      evdref :=
-        Typeclasses.resolve_typeclasses ~onlyargs:false
-	  ~split:true ~fail:fail_evar env !evdref;
+    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
@@ -701,7 +704,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
   let understand_judgment sigma env c =
     let evdref = ref (create_evar_defs sigma) in
     let j = pretype empty_tycon env evdref ([],[]) c in
-    let evd,_ = consider_remaining_unif_problems env !evdref in
+    let evd = consider_remaining_unif_problems env !evdref in
     let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~split:false
       ~fail:true env evd
     in
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index ea6b43fb..7d08026f 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: pretyping.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 492d9a73..afb942fb 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: rawterm.ml 13329 2010-07-26 11:05:39Z herbelin $ *)
 
 (*i*)
 open Util
@@ -34,8 +34,6 @@ type patvar = identifier
 
 type rawsort = RProp of Term.contents | RType of Univ.universe option
 
-type binder_kind = BProd | BLambda | BLetIn
-
 type binding_kind = Lib.binding_kind = Explicit | Implicit
 
 type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier
@@ -185,6 +183,36 @@ let map_rawconstr_with_binders_loc loc g f e = function
   | RDynamic (_,x) -> RDynamic (loc,x)
 *)
 
+let fold_rawconstr f acc =
+  let rec fold acc = function
+  | RVar _ -> acc
+  | RApp (_,c,args) -> List.fold_left fold (fold acc c) args
+  | RLambda (_,_,_,b,c) | RProd (_,_,_,b,c) | RLetIn (_,_,b,c) ->
+      fold (fold acc b) c
+  | RCases (_,_,rtntypopt,tml,pl) ->
+      List.fold_left fold_pattern
+	(List.fold_left fold (Option.fold_left fold acc rtntypopt) (List.map fst tml))
+	pl
+    | RLetTuple (_,_,rtntyp,b,c) ->
+	fold (fold (fold_return_type acc rtntyp) b) c
+    | RIf (_,c,rtntyp,b1,b2) ->
+	fold (fold (fold (fold_return_type acc rtntyp) c) b1) b2
+    | RRec (_,_,_,bl,tyl,bv) ->
+	let acc = Array.fold_left
+	  (List.fold_left (fun acc (na,k,bbd,bty) ->
+	    fold (Option.fold_left fold acc bbd) bty)) acc bl in
+	Array.fold_left fold (Array.fold_left fold acc tyl) bv
+    | RCast (_,c,k) -> fold (match k with CastConv (_, t) -> fold acc t | CastCoerce -> acc) c
+    | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> acc
+
+  and fold_pattern acc (_,idl,p,c) = fold acc c
+
+  and fold_return_type acc (na,tyopt) = Option.fold_left fold acc tyopt
+
+  in fold acc
+
+let iter_rawconstr f = fold_rawconstr (fun () -> f) ()
+
 let occur_rawconstr id =
   let rec occur = function
     | RVar (loc,id') -> id = id'
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index c9dbe4bf..39ff74a3 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: rawterm.mli 13329 2010-07-26 11:05:39Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -38,8 +38,6 @@ type patvar = identifier
 
 type rawsort = RProp of Term.contents | RType of Univ.universe option
 
-type binder_kind = BProd | BLambda | BLetIn
-
 type binding_kind = Lib.binding_kind = Explicit | Implicit
 
 type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier
@@ -110,6 +108,8 @@ val map_rawconstr_with_binders_loc : loc ->
   ('a -> rawconstr -> rawconstr) -> 'a -> rawconstr -> rawconstr
 i*)
 
+val fold_rawconstr : ('a -> rawconstr -> 'a) -> 'a -> rawconstr -> 'a
+val iter_rawconstr : (rawconstr -> unit) -> rawconstr -> unit
 val occur_rawconstr : identifier -> rawconstr -> bool
 val free_rawvars : rawconstr -> identifier list
 val loc_of_rawconstr : rawconstr -> loc
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 47178d06..68ae9208 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: recordops.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Util
 open Pp
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index da883b19..3d97d8b2 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: recordops.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 7519e508..556134de 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: reductionops.ml 13354 2010-07-29 16:44:45Z barras $ *)
 
 open Pp
 open Util
@@ -525,9 +525,11 @@ let nf_evar =
 (* Note by HH [oct 08] : why would it be the job of clos_norm_flags to add
    a [nf_evar] here *)
 let clos_norm_flags flgs env sigma t =
-  norm_val
-    (create_clos_infos ~evars:(safe_evar_value sigma) flgs env)
-    (inject t)
+  try
+    norm_val
+      (create_clos_infos ~evars:(safe_evar_value sigma) flgs env)
+      (inject t)
+  with Anomaly _ -> error "Tried to normalized ill-typed term" 
 
 let nf_beta = clos_norm_flags Closure.beta empty_env
 let nf_betaiota = clos_norm_flags Closure.betaiota empty_env
@@ -586,9 +588,11 @@ let nf_betaiota_preserving_vm_cast =
 
 (* lazy weak head reduction functions *)
 let whd_flags flgs env sigma t =
-  whd_val
-    (create_clos_infos ~evars:(safe_evar_value sigma) flgs env)
-    (inject t)
+  try
+    whd_val
+      (create_clos_infos ~evars:(safe_evar_value sigma) flgs env)
+      (inject t)
+  with Anomaly _ -> error "Tried to normalized ill-typed term" 
 
 (********************************************************************)
 (*                         Conversion                               *)
@@ -620,6 +624,7 @@ let test_conversion (f:?evars:'a->'b) env sigma x y =
   try let _ =
     f ~evars:(safe_evar_value sigma) env x y in true
   with NotConvertible -> false
+    | Anomaly _ -> error "Conversion test raised an anomaly"
 
 let is_conv env sigma = test_conversion Reduction.conv env sigma
 let is_conv_leq env sigma = test_conversion Reduction.conv_leq env sigma
@@ -628,6 +633,7 @@ let is_fconv = function | CONV -> is_conv | CUMUL -> is_conv_leq
 let test_trans_conversion f reds env sigma x y =
   try let _ = f reds env (nf_evar sigma x) (nf_evar sigma y) in true
   with NotConvertible -> false
+    | Anomaly _ -> error "Conversion test raised an anomaly"
 
 let is_trans_conv reds env sigma = test_trans_conversion Reduction.trans_conv reds env sigma
 let is_trans_conv_leq reds env sigma = test_trans_conversion Reduction.trans_conv_leq reds env sigma
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index ab4c6f5d..f557df00 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: reductionops.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index d736031f..e4a85b84 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: retyping.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Util
 open Term
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index 7b53da7e..98a3ff42 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: retyping.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 3089b7ca..49ccb80c 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: tacred.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index d5703d6b..064d2ce4 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: tacred.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index f746245f..a2759688 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: termops.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index f13df9d2..7977fe28 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: termops.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 open Util
 open Pp
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index da17c299..d75032e7 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: typeclasses.ml 13332 2010-07-26 22:12:43Z msozeau $ i*)
 
 (*i*)
 open Names
@@ -106,6 +106,29 @@ let _ =
       Summary.unfreeze_function = unfreeze;
       Summary.init_function = init }
 
+let class_info c =
+  try Gmap.find c !classes
+  with _ -> not_a_class (Global.env()) (constr_of_global c)
+
+let global_class_of_constr env c =
+  try class_info (global_of_constr c)
+  with Not_found -> not_a_class env c
+
+let dest_class_app env c =
+  let cl, args = decompose_app c in
+    global_class_of_constr env cl, args
+
+let class_of_constr c = try Some (fst (dest_class_app (Global.env ()) c)) with _ -> None
+
+let rec is_class_type evd c =
+  match kind_of_term c with
+  | Prod (_, _, t) -> is_class_type evd t
+  | Evar (e, _) when is_defined evd e -> is_class_type evd (Evarutil.nf_evar evd c)
+  | _ -> class_of_constr c <> None
+
+let is_class_evar evd evi =
+  is_class_type evd evi.Evd.evar_concl
+
 (*
  * classes persistent object
  *)
@@ -153,8 +176,15 @@ let discharge_class (_,cl) =
       | ConstRef cst -> Lib.section_segment_of_constant cst
       | IndRef (ind,_) -> Lib.section_segment_of_mutual_inductive ind in
   let discharge_context ctx' subst (grs, ctx) =
-    let grs' = List.map (fun _ -> None) subst @
-      list_smartmap (Option.smartmap (fun (gr, b) -> Lib.discharge_global gr, b)) grs
+    let grs' = 
+      let newgrs = List.map (fun (_, _, t) -> 
+	match class_of_constr t with
+	| None -> None
+	| Some tc -> Some (tc.cl_impl, true))
+	ctx' 
+      in
+	list_smartmap (Option.smartmap (fun (gr, b) -> Lib.discharge_global gr, b)) grs
+	  @ newgrs
     in grs', discharge_rel_context subst 1 ctx @ ctx' in
   let cl_impl' = Lib.discharge_global cl.cl_impl in
   if cl_impl' == cl.cl_impl then cl else
@@ -265,10 +295,6 @@ let add_inductive_class ind =
  * interface functions
  *)
 
-let class_info c =
-  try Gmap.find c !classes
-  with _ -> not_a_class (Global.env()) (constr_of_global c)
-
 let instance_constructor cl args =
   let lenpars = List.length (List.filter (fun (na, b, t) -> b = None) (snd cl.cl_context)) in
   let pars = fst (list_chop lenpars args) in
@@ -322,16 +348,6 @@ let is_implicit_arg k =
     | InternalHole -> true
     | _ -> false
 
-let global_class_of_constr env c =
-  try class_info (global_of_constr c)
-  with Not_found -> not_a_class env c
-
-let dest_class_app env c =
-  let cl, args = decompose_app c in
-    global_class_of_constr env cl, args
-
-let class_of_constr c = try Some (fst (dest_class_app (Global.env ()) c)) with _ -> None
-
 (* To embed a boolean for resolvability status.
    This is essentially a hack to mark which evars correspond to
    goals and do not need to be resolved when we have nested [resolve_all_evars]
@@ -356,15 +372,6 @@ let mark_unresolvables sigma =
     Evd.add evs ev (mark_unresolvable evi))
     sigma Evd.empty
 
-let rec is_class_type evd c =
-  match kind_of_term c with
-  | Prod (_, _, t) -> is_class_type evd t
-  | Evar (e, _) when is_defined evd e -> is_class_type evd (Evarutil.nf_evar evd c)
-  | _ -> class_of_constr c <> None
-
-let is_class_evar evd evi =
-  is_class_type evd evi.Evd.evar_concl
-
 let has_typeclasses evd =
   Evd.fold (fun ev evi has -> has ||
     (evi.evar_body = Evar_empty && is_class_evar evd evi && is_resolvable evi))
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 80387ec5..8e1c2a92 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: typeclasses.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index eb24c731..b3ab1f07 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: typeclasses_errors.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index 4ec5ad70..94e1a57d 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: typeclasses_errors.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 43880615..82b59d16 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: typing.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Util
 open Names
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 49a6a23e..32b64c5f 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: typing.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Term
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index a096a074..02af6090 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: unification.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
 
 open Pp
 open Util
@@ -573,12 +573,9 @@ let is_mimick_head f =
 let try_to_coerce env evd c cty tycon =
   let j = make_judge c cty in
   let (evd',j') = inh_conv_coerce_rigid_to dummy_loc env evd j tycon in
-  let (evd',b) = Evarconv.consider_remaining_unif_problems env evd' in
-  if b then
-    let evd' = Evd.map_metas_fvalue (nf_evar evd') evd' in
+  let evd' = Evarconv.consider_remaining_unif_problems env evd' in
+  let evd' = Evd.map_metas_fvalue (nf_evar evd') evd' in
     (evd',j'.uj_val)
-  else
-    error "Cannot solve unification constraints"
 
 let w_coerce_to_type env evd c cty mvty =
   let evd,mvty = pose_all_metas_as_evars env evd mvty in
@@ -634,9 +631,7 @@ let order_metas metas =
 let solve_simple_evar_eqn env evd ev rhs =
   let evd,b = solve_simple_eqn Evarconv.evar_conv_x env evd (None,ev,rhs) in
   if not b then error_cannot_unify env evd (mkEvar ev,rhs);
-  let (evd,b) = Evarconv.consider_remaining_unif_problems env evd in
-  if not b then error "Cannot solve unification constraints";
-  evd
+  Evarconv.consider_remaining_unif_problems env evd
 
 (* [w_merge env sigma b metas evars] merges common instances in metas
    or in evars, possibly generating new unification problems; if [b]
@@ -656,11 +651,16 @@ let w_merge env with_types flags (evd,metas,evars) =
     	else begin
           let rhs' = subst_meta_instances metas rhs in
           match kind_of_term rhs with
-	  | App (f,cl) when is_mimick_head f & occur_meta rhs' ->
+	  | App (f,cl) when occur_meta rhs' ->
 	      if occur_evar evn rhs' then
                 error_occur_check env evd evn rhs';
-	      let evd' = mimick_evar evd flags f (Array.length cl) evn in
-	      w_merge_rec evd' metas evars eqns
+	      if is_mimick_head f then
+		let evd' = mimick_evar evd flags f (Array.length cl) evn in
+		  w_merge_rec evd' metas evars eqns
+	      else
+		let evd', rhs'' = pose_all_metas_as_evars env evd rhs' in
+	  	  w_merge_rec (solve_simple_evar_eqn env evd' ev rhs'')
+		    metas evars' eqns
           | _ ->
 	      w_merge_rec (solve_simple_evar_eqn env evd ev rhs')
 		metas evars' eqns
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 7a91ce66..419d5d4f 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: unification.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Term
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 2de542cd..2c8705d5 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: vnorm.ml 13351 2010-07-29 15:26:31Z barras $ i*)
 
 open Names
 open Declarations
@@ -117,7 +117,7 @@ let build_branches_type env (mind,_ as _ind) mib mip params dep p =
     let carity = snd (rtbl.(i)) in
     let crealargs = Array.sub cargs nparams (Array.length cargs - nparams) in
     let codom =
-      let papp = mkApp(p,crealargs) in
+      let papp = mkApp(lift (List.length decl) p,crealargs) in
       if dep then
 	let cstr = ith_constructor_of_inductive ind (i+1) in
         let relargs = Array.init carity (fun i -> mkRel (carity-i)) in