Imported Upstream version 8.3.pl3upstream/8.3.pl3

56 files changed, 180 insertions, 165 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 67bf7043..749101f7 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: cases.ml 13962 2011-04-06 17:00:45Z herbelin $ *)
+(* $Id: cases.ml 14675 2011-11-17 22:19:34Z herbelin $ *)
 
 open Util
 open Names
@@ -409,15 +409,14 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) =
      the first pattern type and forget about the others *)
   let typ,names =
     match typ with IsInd(t,_,names) -> t,Some names | NotInd(_,t) -> t,None in
-  let typ =
+  let tmtyp =
     try try_find_ind pb.env !(pb.evdref) typ names
     with Not_found -> NotInd (None,typ) in
-  let tomatch = ((current,typ),deps,dep) in
-  match typ with
+  match tmtyp with
   | NotInd (None,typ) ->
       let tm1 = List.map (fun eqn -> List.hd eqn.patterns) pb.mat in
       (match find_row_ind tm1 with
-	| None -> tomatch
+	| None -> (current,tmtyp)
 	| Some (_,(ind,_)) ->
 	    let indt = inductive_template pb.evdref pb.env None ind in
 	    let current =
@@ -429,9 +428,8 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) =
 		(evd_comb2 (Coercion.inh_conv_coerce_to dummy_loc pb.env)
 		  pb.evdref (make_judge current typ) (mk_tycon_type indt)).uj_val in
 	    let sigma =  !(pb.evdref) in
-	    let typ = try_find_ind pb.env sigma indt names in
-	    ((current,typ),deps,dep))
-  | _ -> tomatch
+	    (current,try_find_ind pb.env sigma indt names))
+  | _ -> (current,tmtyp)
 
 let type_of_tomatch = function
   | IsInd (t,_,_) -> t
@@ -875,22 +873,24 @@ let generalize_predicate (names,(nadep,_)) ny d tms ccl =
   let ccl = lift_predicate 1 ccl tms in
   regeneralize_index_predicate (ny+p+1) ccl tms
 
-let rec extract_predicate l ccl = function
-  | Alias (deppat,nondeppat,_,_)::tms ->
-      let tms' = match kind_of_term nondeppat with
-        | Rel i -> replace_tomatch i deppat tms
-        | _ -> (* initial terms are not dependent *) tms in
-      extract_predicate l ccl tms'
-  | Abstract d'::tms ->
-      let d' = map_rel_declaration (lift (List.length l)) d' in
-      substl l (mkProd_or_LetIn d' (extract_predicate [] ccl tms))
+let rec extract_predicate ccl = function
+   | Alias (deppat,nondeppat,_,_)::tms ->
+       (* substitution already done in build_branch *)
+      extract_predicate ccl tms
+  | Abstract d::tms ->
+      mkProd_or_LetIn d (extract_predicate ccl tms)
   | Pushed ((cur,NotInd _),_,(dep,_))::tms ->
-      extract_predicate (if dep<>Anonymous then cur::l else l) ccl tms
+      let tms = if dep<>Anonymous then lift_tomatch_stack 1 tms else tms in
+      let pred = extract_predicate ccl tms in
+      if dep<>Anonymous then subst1 cur pred else pred
   | Pushed ((cur,IsInd (_,IndType(_,realargs),_)),_,(dep,_))::tms ->
-      let l = List.rev realargs@l in
-      extract_predicate (if dep<>Anonymous then cur::l else l) ccl tms
+      let realargs = List.rev realargs in
+      let k = if dep<>Anonymous then 1 else 0 in
+      let tms = lift_tomatch_stack (List.length realargs + k) tms in
+      let pred = extract_predicate ccl tms in
+      substl (if dep<>Anonymous then cur::realargs else realargs) pred
   | [] ->
-      substl l ccl
+      ccl
 
 let abstract_predicate env sigma indf cur (names,(nadep,_)) tms ccl =
   let sign = make_arity_signature env true indf in
@@ -903,7 +903,7 @@ let abstract_predicate env sigma indf cur (names,(nadep,_)) tms ccl =
       | _ -> (* Initial case *) tms in
   let sign = List.map2 (fun na (_,c,t) -> (na,c,t)) (nadep::names) sign in
   let ccl = if nadep <> Anonymous then ccl else lift_predicate 1 ccl tms in
-  let pred = extract_predicate [] ccl tms in
+  let pred = extract_predicate ccl tms in
   it_mkLambda_or_LetIn_name env pred sign
 
 let known_dependent (_,dep) = (dep = KnownDep)
@@ -982,14 +982,18 @@ let find_predicate loc env evdref p current (IndType (indf,realargs)) dep tms =
   (pred, whd_betaiota !evdref
            (applist (pred, realargs@[current])), new_Type ())
 
-let adjust_predicate_from_tomatch ((_,oldtyp),_,(nadep,_)) typ pb =
+(* Take into account that a type has been discovered to be inductive, leading
+   to more dependencies in the predicate if the type has indices *)
+let adjust_predicate_from_tomatch tomatch (current,typ as ct) pb =
+  let ((_,oldtyp),deps,((nadep,_) as dep)) = tomatch in
   match typ, oldtyp with
   | IsInd (_,_,names), NotInd _ ->
       let k = if nadep <> Anonymous then 2 else 1 in
       let n = List.length names in
-      { pb with	pred = liftn_predicate n k pb.pred pb.tomatch }
+      { pb with pred = liftn_predicate n k pb.pred pb.tomatch },
+      (ct,List.map (fun i -> if i >= k then i+n else i) deps,dep)
   | _ ->
-      pb
+      pb, (ct,deps,dep)
 
 (************************************************************************)
 (* Sorting equations by constructor *)
@@ -1105,6 +1109,10 @@ let build_branch current deps (realnames,dep) pb arsign eqns const_info =
   (* into  "Gamma; typs; curalias |- tms" *)
   let tomatch = lift_tomatch_stack const_info.cs_nargs pb.tomatch in
 
+  let tomatch = match kind_of_term current with
+    | Rel i -> replace_tomatch (i+const_info.cs_nargs) ci tomatch
+    | _ -> (* non-rel initial term *) tomatch in
+
   let pred_is_not_dep =
     noccur_predicate_between 1 (List.length realnames + 1) pb.pred tomatch in
 
@@ -1171,20 +1179,22 @@ let rec compile pb =
     | (Abstract d)::rest -> compile_generalization pb d rest
     | [] -> build_leaf pb
 
+(* Case splitting *)
 and match_current pb tomatch =
-  let ((current,typ),deps,dep as ct) = adjust_tomatch_to_pattern pb tomatch in
-  let pb = adjust_predicate_from_tomatch tomatch typ pb in
+  let tm = adjust_tomatch_to_pattern pb tomatch in
+  let pb,tomatch = adjust_predicate_from_tomatch tomatch tm pb in
+  let ((current,typ),deps,dep) = tomatch in
   match typ with
     | NotInd (_,typ) ->
 	check_all_variables typ pb.mat;
-	compile (shift_problem ct pb)
+	compile (shift_problem tomatch pb)
     | IsInd (_,(IndType(indf,realargs) as indt),names) ->
 	let mind,_ = dest_ind_family indf in
 	let cstrs = get_constructors pb.env indf in
 	let arsign, _ = get_arity pb.env indf in
 	let eqns,onlydflt = group_equations pb mind current cstrs pb.mat in
 	if (Array.length cstrs <> 0 or pb.mat <> []) & onlydflt  then
-	  compile (shift_problem ct pb)
+	  compile (shift_problem tomatch pb)
 	else
           let _constraints = Array.map (solve_constraints indt) cstrs in
 
@@ -1220,21 +1230,11 @@ and compile_generalization pb d rest =
   { uj_val = mkLambda_or_LetIn d j.uj_val;
     uj_type = mkProd_or_LetIn d j.uj_type }
 
-and compile_alias pb (deppat,nondeppat,d,t) rest =
+and compile_alias pb aliases rest =
   let history = simplify_history pb.history in
-  let sign, newenv, mat =
-    insert_aliases pb.env !(pb.evdref) (deppat,nondeppat,d,t) pb.mat in
+  let sign, newenv, mat = insert_aliases pb.env !(pb.evdref) aliases pb.mat in
   let n = List.length sign in
-
-  (* We had Gamma1; x:current; Gamma2 |- tomatch(x) and we rebind x to get *)
-  (* Gamma1; x:current; Gamma2; typs; x':=curalias |- tomatch(x') *)
   let tomatch = lift_tomatch_stack n rest in
-  let tomatch = match kind_of_term nondeppat with
-    | Rel i ->
-	if n = 1 then regeneralize_index_tomatch (i+n) tomatch
-	else replace_tomatch i deppat tomatch
-    | _ -> (* initial terms are not dependent *) tomatch in
-
   let pb =
     {pb with
        env = newenv;
@@ -1395,7 +1395,10 @@ let build_tycon loc env tycon_env subst tycon extenv evdref t =
 	  e_new_evar evdref env ~src:(loc,ImpossibleCase) (new_Type ()) in
 	lift (n'-n) impossible_case_type
     | Some t -> abstract_tycon loc tycon_env evdref subst tycon extenv t in
-  get_judgment_of extenv !evdref t
+  try get_judgment_of extenv !evdref t
+  with Not_found | Anomaly _ ->
+    (* Quick workaround to acknowledge failure to build a well-typed pred *)
+    error "Unable to infer a well-typed return clause."
 
 (* For a multiple pattern-matching problem Xi on t1..tn with return
  * type T, [build_inversion_problem Gamma Sigma (t1..tn) T] builds a return
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 7bc635fb..2711276a 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: cases.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: cases.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Util
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index ec71159b..802f9c58 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: cbv.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: cbv.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Util
 open Pp
diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli
index 5486b064..e66e6dc6 100644
--- a/pretyping/cbv.mli
+++ b/pretyping/cbv.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: cbv.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: cbv.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 17f18a9b..504d01af 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: classops.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: classops.ml 14776 2011-12-07 17:54:28Z herbelin $ *)
 
 open Util
 open Pp
@@ -369,8 +369,8 @@ let load_coercion _ o =
   then
     cache_coercion o
 
-let open_coercion _ o =
-  if not
+let open_coercion i o =
+  if i = 1 && not
     (!automatically_import_coercions || Flags.version_less_or_equal Flags.V8_2)
   then
     cache_coercion o
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index f905e392..964b44a0 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: classops.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: classops.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index b9fd307c..abfef8d4 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: clenv.ml 13902 2011-03-10 15:50:24Z msozeau $ *)
+(* $Id: clenv.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index b50e313c..6fbb668b 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: clenv.mli 13332 2010-07-26 22:12:43Z msozeau $ i*)
+(*i $Id: clenv.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Util
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index dd099aa1..d0f20615 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -1,11 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(* $Id: coercion.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: coercion.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Util
 open Names
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index 00848dac..6ad1023e 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: coercion.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: coercion.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Util
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index e435484e..14e72807 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: detyping.ml 13329 2010-07-26 11:05:39Z herbelin $ *)
+(* $Id: detyping.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Pp
 open Util
@@ -467,7 +467,7 @@ and share_names isgoal n l avoid env c t =
         let b = detype isgoal avoid env b in
 	let id = next_name_away na avoid in
         let avoid = id::avoid and env = add_name (Name id) env in
-        share_names isgoal n ((Name id,Explicit,Some b,t')::l) avoid env c t
+        share_names isgoal n ((Name id,Explicit,Some b,t')::l) avoid env c (lift 1 t)
     (* Only if built with the f/n notation or w/o let-expansion in types *)
     | _, LetIn (_,b,_,t) when n > 0 ->
 	share_names isgoal n l avoid env c (subst1 b t)
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index cdb840b6..556b2477 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: detyping.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: detyping.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Util
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 51183be3..6d080016 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evarconv.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
+(* $Id: evarconv.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index b0702038..50228d4e 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: evarconv.mli 13332 2010-07-26 22:12:43Z msozeau $ i*)
+(*i $Id: evarconv.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Term
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 09ec8dda..b95b50b3 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evarutil.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
+(* $Id: evarutil.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Util
 open Pp
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index d677b972..e29effc2 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: evarutil.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: evarutil.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Util
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 5d61e727..2db77837 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evd.ml 13902 2011-03-10 15:50:24Z msozeau $ *)
+(* $Id: evd.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index c68cfffe..8a903f1b 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: evd.mli 13902 2011-03-10 15:50:24Z msozeau $ i*)
+(*i $Id: evd.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Util
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 927af594..edbab0a7 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: indrec.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: indrec.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 (* File initially created by Christine Paulin, 1996 *)
 
diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli
index 188ad74d..b2375c8f 100644
--- a/pretyping/indrec.mli
+++ b/pretyping/indrec.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: indrec.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: indrec.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 85c865fa..6e54c170 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: inductiveops.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: inductiveops.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Util
 open Names
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 251c6b2e..e5759864 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: inductiveops.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: inductiveops.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 open Names
 open Term
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index 6ee67bf2..f0536f22 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: matching.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: matching.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 (*i*)
 open Util
diff --git a/pretyping/matching.mli b/pretyping/matching.mli
index 25863129..fc0e3feb 100644
--- a/pretyping/matching.mli
+++ b/pretyping/matching.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: matching.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: matching.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
index 6e3e2f7c..45060511 100644
--- a/pretyping/namegen.ml
+++ b/pretyping/namegen.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: namegen.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: namegen.ml 14641 2011-11-06 11:59:10Z 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 419624b8..f99ee3f6 100644
--- a/pretyping/namegen.mli
+++ b/pretyping/namegen.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: namegen.mli 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: namegen.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Names
 open Term
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index d1c4cfc1..83bfe9ea 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pattern.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: pattern.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Util
 open Names
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index fbc6bbaa..195fecfe 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: pattern.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: pattern.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Pp
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 6befdedc..688a25b9 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pretype_errors.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: pretype_errors.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Util
 open Stdpp
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 496e16d2..d3e6ffea 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: pretype_errors.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: pretype_errors.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Pp
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index b8dc719b..a3b1dd18 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pretyping.ml 13780 2011-01-07 16:37:57Z herbelin $ *)
+(* $Id: pretyping.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 7d08026f..b94f9789 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: pretyping.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: pretyping.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index afb942fb..978dbeef 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: rawterm.ml 13329 2010-07-26 11:05:39Z herbelin $ *)
+(* $Id: rawterm.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 (*i*)
 open Util
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 39ff74a3..10156cec 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: rawterm.mli 13329 2010-07-26 11:05:39Z herbelin $ i*)
+(*i $Id: rawterm.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Util
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 68ae9208..e8c6073e 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: recordops.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: recordops.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Util
 open Pp
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 78626854..b71c4969 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: recordops.mli 13447 2010-09-21 13:23:45Z letouzey $ i*)
+(*i $Id: recordops.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 556134de..5af20551 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: reductionops.ml 13354 2010-07-29 16:44:45Z barras $ *)
+(* $Id: reductionops.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index f557df00..95032bde 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: reductionops.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: reductionops.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index e4a85b84..7fb4f7ba 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: retyping.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: retyping.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Util
 open Term
@@ -44,7 +44,7 @@ let type_of_var env id =
   with Not_found ->
     anomaly ("type_of: variable "^(string_of_id id)^" unbound")
 
-let retype sigma =
+let retype ?(polyprop=true) sigma =
   let rec type_of env cstr=
     match kind_of_term cstr with
     | Meta n ->
@@ -129,7 +129,7 @@ let retype sigma =
     match kind_of_term c with
     | Ind ind ->
       let (_,mip) = lookup_mind_specif env ind in
-      Inductive.type_of_inductive_knowing_parameters env mip argtyps
+      Inductive.type_of_inductive_knowing_parameters ~polyprop env mip argtyps
     | Const cst ->
       let t = constant_type env cst in
       Typeops.type_of_constant_knowing_parameters env t argtyps
@@ -140,8 +140,10 @@ let retype sigma =
   in type_of, sort_of, sort_family_of,
      type_of_global_reference_knowing_parameters
 
-let get_sort_of env sigma t = let _,f,_,_ = retype sigma in f env t
-let get_sort_family_of env sigma c = let _,_,f,_ = retype sigma in f env c
+let get_sort_of ?(polyprop=true) env sigma t =
+  let _,f,_,_ = retype ~polyprop sigma in f env t
+let get_sort_family_of ?(polyprop=true) env sigma c =
+  let _,_,f,_ = retype ~polyprop sigma in f env c
 let type_of_global_reference_knowing_parameters env sigma c args =
   let _,_,_,f = retype sigma in f env c args
 
@@ -161,8 +163,8 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty =
 
 (* We are outside the kernel: we take fresh universes *)
 (* to avoid tactics and co to refresh universes themselves *)
-let get_type_of ?(refresh=true) env sigma c =
-  let f,_,_,_ = retype sigma in
+let get_type_of ?(polyprop=true) ?(refresh=true) env sigma c =
+  let f,_,_,_ = retype ~polyprop sigma in
   let t = f env c in
     if refresh then refresh_universes t else t
 
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index 98a3ff42..f2c030f9 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: retyping.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: retyping.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -21,9 +21,17 @@ open Environ
    either produces a wrong result or raise an anomaly. Use with care.
    It doesn't handle predicative universes too. *)
 
-val get_type_of : ?refresh:bool -> env -> evar_map -> constr -> types
-val get_sort_of : env -> evar_map -> types -> sorts
-val get_sort_family_of : env -> evar_map -> types -> sorts_family
+(** The "polyprop" optional argument is used by the extraction to
+    disable "Prop-polymorphism", cf comment in [inductive.ml] *)
+
+val get_type_of :
+  ?polyprop:bool -> ?refresh:bool -> env -> evar_map -> constr -> types
+
+val get_sort_of :
+  ?polyprop:bool -> env -> evar_map -> types -> sorts
+
+val get_sort_family_of :
+  ?polyprop:bool -> env -> evar_map -> types -> sorts_family
 
 (* Makes an assumption from a constr *)
 val get_assumption_of : env -> evar_map -> constr -> types
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 68a67402..bd1eed94 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tacred.ml 13804 2011-01-27 00:41:34Z letouzey $ *)
+(* $Id: tacred.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 064d2ce4..55c305cc 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: tacred.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: tacred.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/pretyping/term_dnet.ml b/pretyping/term_dnet.ml
index 0dfee738..9dda5143 100644
--- a/pretyping/term_dnet.ml
+++ b/pretyping/term_dnet.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/term_dnet.mli b/pretyping/term_dnet.mli
index a8ac4119..9c4c9dbc 100644
--- a/pretyping/term_dnet.mli
+++ b/pretyping/term_dnet.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index a2759688..70f2279c 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: termops.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: termops.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 7977fe28..91c76564 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: termops.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: termops.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 open Util
 open Pp
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index d75032e7..9e64143d 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: typeclasses.ml 13332 2010-07-26 22:12:43Z msozeau $ i*)
+(*i $Id: typeclasses.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -299,9 +299,11 @@ 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
     match cl.cl_impl with
-      | IndRef ind -> applistc (mkConstruct (ind, 1)) args,
+      | IndRef ind -> Some (applistc (mkConstruct (ind, 1)) args),
 	  applistc (mkInd ind) pars
-      | ConstRef cst -> list_last args, applistc (mkConst cst) pars
+      | ConstRef cst -> 
+	let term = if args = [] then None else Some (list_last args) in
+	  term, applistc (mkConst cst) pars
       | _ -> assert false
 
 let typeclasses () = Gmap.fold (fun _ l c -> l :: c) !classes []
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 8e1c2a92..83ae84a5 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: typeclasses.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: typeclasses.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -75,7 +75,7 @@ val is_implicit_arg : hole_kind -> bool
 (* Returns the term and type for the given instance of the parameters and fields
    of the type class. *)
 
-val instance_constructor : typeclass -> constr list -> constr * types
+val instance_constructor : typeclass -> constr list -> constr option * types
 
 (* Use evar_extra for marking resolvable evars. *)
 val bool_in : bool -> Dyn.t
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index b3ab1f07..62941a76 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: typeclasses_errors.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: typeclasses_errors.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index 94e1a57d..a763a80b 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: typeclasses_errors.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: typeclasses_errors.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 82b59d16..80db26a4 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: typing.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: typing.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Util
 open Names
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 32b64c5f..07cb7d59 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: typing.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: typing.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Term
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 02af6090..7aa2272d 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: unification.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
+(* $Id: unification.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 419d5d4f..2f48081a 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: unification.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: unification.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Term
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 2c8705d5..395f5c8d 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: vnorm.ml 13351 2010-07-29 15:26:31Z barras $ i*)
+(*i $Id: vnorm.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 open Names
 open Declarations
diff --git a/pretyping/vnorm.mli b/pretyping/vnorm.mli
index ec8af8d4..4cf99842 100644
--- a/pretyping/vnorm.mli
+++ b/pretyping/vnorm.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)