Remove non-DFSG contentsupstream/8.3.pl4+dfsg

9 files changed, 56 insertions, 63 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 749101f7..4205f517 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: cases.ml 14675 2011-11-17 22:19:34Z herbelin $ *)
+(* $Id: cases.ml 15025 2012-03-09 14:27:07Z glondu $ *)
 
 open Util
 open Names
@@ -100,7 +100,7 @@ let rec list_try_compile f = function
   | h::t ->
       try f h
       with UserError _ | TypeError _ | PretypeError _
-	| Stdpp.Exc_located (_,(UserError _ | TypeError _ | PretypeError _)) ->
+	| Compat.Exc_located (_,(UserError _ | TypeError _ | PretypeError _)) ->
 	    list_try_compile f t
 
 let force_name =
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index abfef8d4..c2dd9f03 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: clenv.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: clenv.ml 15069 2012-03-20 14:06:07Z herbelin $ *)
 
 open Pp
 open Util
@@ -146,9 +146,6 @@ let mk_clenv_from_n gls n (c,cty) =
 
 let mk_clenv_from gls = mk_clenv_from_n gls None
 
-let mk_clenv_rename_from_n gls n (c,t) =
-  mk_clenv_from_n gls n (c,rename_bound_vars_as_displayed [] t)
-
 let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t)
 
 (******************************************************************)
@@ -460,8 +457,8 @@ let make_clenv_binding_gen hyps_only n env sigma (c,t) = function
       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_from_env env sigma n 
-	(c,rename_bound_vars_as_displayed [] t) 
+      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_env env sigma n (c,t)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 14e72807..fe4354b6 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: detyping.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: detyping.ml 15069 2012-03-20 14:06:07Z herbelin $ *)
 
 open Pp
 open Util
@@ -533,7 +533,7 @@ and detype_eqn isgoal avoid env constr construct_nargs branch =
   buildrec [] [] avoid env construct_nargs branch
 
 and detype_binder isgoal bk avoid env na ty c =
-  let flag = if isgoal then RenamingForGoal else (RenamingElsewhereFor c) in
+  let flag = if isgoal then RenamingForGoal else RenamingElsewhereFor (env,c) in
   let na',avoid' =
     if bk = BLetIn then compute_displayed_let_name_in flag avoid na c
     else compute_displayed_name_in flag avoid na c in
@@ -553,9 +553,11 @@ let rec detype_rel_context where avoid env sign =
 	| None -> na,avoid
 	| Some c ->
 	    if b<>None then
-	      compute_displayed_let_name_in (RenamingElsewhereFor c) avoid na c
+	      compute_displayed_let_name_in
+                (RenamingElsewhereFor (env,c)) avoid na c
 	    else
-	      compute_displayed_name_in (RenamingElsewhereFor c) avoid na c in
+	      compute_displayed_name_in
+                (RenamingElsewhereFor (env,c)) avoid na c in
       let b = Option.map (detype false avoid env) b in
       let t = detype false avoid env t in
       (na',Explicit,b,t) :: aux avoid' (add_name na' env) rest
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 6e54c170..fe90941d 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: inductiveops.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: inductiveops.ml 15019 2012-03-02 17:27:18Z letouzey $ *)
 
 open Util
 open Names
@@ -403,21 +403,6 @@ let arity_of_case_predicate env (ind,params) dep k =
 (* Inferring the sort of parameters of a polymorphic inductive type
    knowing the sort of the conclusion *)
 
-(* Check if u (sort of a parameter) appears in the sort of the
-   inductive (is). This is done by trying to enforce u > u' >= is
-   in the empty univ graph. If an inconsistency appears, then
-   is depends on u. *)
-let is_constrained is u =
-  try
-    let u' = fresh_local_univ() in
-    let _ =
-      merge_constraints
-        (enforce_geq u (super u')
-          (enforce_geq u' is Constraint.empty))
-        initial_universes in
-    false
-  with UniverseInconsistency _ -> true
-
 (* Compute the inductive argument types: replace the sorts
    that appear in the type of the inductive by the sort of the
    conclusion, and the other ones by fresh universes. *)
@@ -429,7 +414,9 @@ let rec instantiate_universes env scl is = function
   | (na,None,ty)::sign, Some u::exp ->
       let ctx,_ = Reduction.dest_arity env ty in
       let s =
-        if is_constrained is u then
+	(* Does the sort of parameter [u] appear in (or equal)
+           the sort of inductive [is] ? *)
+        if univ_depends u is then
           scl (* constrained sort: replace by scl *)
         else
           (* unconstriained sort: replace by fresh universe *)
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
index 45060511..f133d842 100644
--- a/pretyping/namegen.ml
+++ b/pretyping/namegen.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: namegen.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: namegen.ml 15069 2012-03-20 14:06:07Z herbelin $ *)
 
 (* Created from contents that was formerly in termops.ml and
    nameops.ml, Nov 2009 *)
@@ -223,22 +223,27 @@ let make_all_name_different env =
    looks for name of same base with lower available subscript beyond current
    subscript *)
 
-let visibly_occur_id id c =
-  let rec occur c = match kind_of_term c with
+let occur_rel p env id =
+  try lookup_name_of_rel p env = Name id
+  with Not_found -> false (* Unbound indice : may happen in debug *)
+
+let visibly_occur_id id (nenv,c) =
+  let rec occur n c = match kind_of_term c with
     | Const _ | Ind _ | Construct _ | Var _
 	  when shortest_qualid_of_global Idset.empty (global_of_constr c)
 	    = qualid_of_ident id -> raise Occur
-    | _ -> iter_constr occur c
+    | Rel p when p>n & occur_rel (p-n) nenv id -> raise Occur
+    | _ -> iter_constr_with_binders succ occur n c
   in
-  try occur c; false
+  try occur 1 c; false
   with Occur -> true
     | Not_found -> false (* Happens when a global is not in the env *)
 
-let next_ident_away_for_default_printing t id avoid =
-  let bad id = List.mem id avoid or visibly_occur_id id t in
+let next_ident_away_for_default_printing env_t id avoid =
+  let bad id = List.mem id avoid or visibly_occur_id id env_t in
   next_ident_away_from id bad
 
-let next_name_away_for_default_printing t na avoid =
+let next_name_away_for_default_printing env_t na avoid =
   let id = match na with
   | Name id   -> id
   | Anonymous ->
@@ -246,7 +251,7 @@ let next_name_away_for_default_printing t na avoid =
       (* taken into account by the function compute_displayed_name_in; *)
       (* just in case, invent a valid name *)
       id_of_string "H" in
-  next_ident_away_for_default_printing t id avoid
+  next_ident_away_for_default_printing env_t id avoid
 
 (**********************************************************************)
 (* Displaying terms avoiding bound variables clashes *)
@@ -269,13 +274,13 @@ let next_name_away_for_default_printing t na avoid =
 type renaming_flags =
   | RenamingForCasesPattern
   | RenamingForGoal
-  | RenamingElsewhereFor of constr
+  | RenamingElsewhereFor of (name list * constr)
 
 let next_name_for_display flags =
   match flags with
   | RenamingForCasesPattern -> next_name_away_in_cases_pattern
   | RenamingForGoal -> next_name_away_in_goal
-  | RenamingElsewhereFor t -> next_name_away_for_default_printing t
+  | RenamingElsewhereFor env_t -> next_name_away_for_default_printing env_t
 
 (* Remark: Anonymous var may be dependent in Evar's contexts *)
 let compute_displayed_name_in flags avoid na c =
@@ -297,16 +302,20 @@ let compute_displayed_let_name_in flags avoid na c =
   let fresh_id = next_name_for_display flags na avoid in
   (Name fresh_id, fresh_id::avoid)
 
-let rec rename_bound_vars_as_displayed avoid c =
-  let rec rename avoid c =
+let rec rename_bound_vars_as_displayed avoid env c =
+  let rec rename avoid env c =
     match kind_of_term c with
     | Prod (na,c1,c2)  ->
-	let na',avoid' = compute_displayed_name_in (RenamingElsewhereFor c2) avoid na c2 in
-	mkProd (na', c1, rename avoid' c2)
+	let na',avoid' =
+          compute_displayed_name_in
+            (RenamingElsewhereFor (env,c2)) avoid na c2 in
+	mkProd (na', c1, rename avoid' (add_name na' env) c2)
     | LetIn (na,c1,t,c2) ->
-	let na',avoid' = compute_displayed_let_name_in (RenamingElsewhereFor c2) avoid na c2 in
-	mkLetIn (na',c1,t, rename avoid' c2)
-    | Cast (c,k,t) -> mkCast (rename avoid c, k,t)
+	let na',avoid' =
+          compute_displayed_let_name_in
+            (RenamingElsewhereFor (env,c2)) avoid na c2 in
+	mkLetIn (na',c1,t, rename avoid' (add_name na' env) c2)
+    | Cast (c,k,t) -> mkCast (rename avoid env c, k,t)
     | _ -> c
   in
-  rename avoid c
+  rename avoid env c
diff --git a/pretyping/namegen.mli b/pretyping/namegen.mli
index f99ee3f6..464efcf8 100644
--- a/pretyping/namegen.mli
+++ b/pretyping/namegen.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: namegen.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: namegen.mli 15069 2012-03-20 14:06:07Z herbelin $ *)
 
 open Names
 open Term
@@ -64,7 +64,7 @@ val next_name_away_with_default : string -> name -> identifier list ->
 type renaming_flags =
   | RenamingForCasesPattern (* avoid only global constructors *)
   | RenamingForGoal (* avoid all globals (as in intro) *)
-  | RenamingElsewhereFor of constr
+  | RenamingElsewhereFor of (name list * constr)
 
 val make_all_name_different : env -> env
 
@@ -74,4 +74,5 @@ val compute_and_force_displayed_name_in :
   renaming_flags -> identifier list -> name -> constr -> name * identifier list
 val compute_displayed_let_name_in :
   renaming_flags -> identifier list -> name -> constr -> name * identifier list
-val rename_bound_vars_as_displayed : identifier list -> types -> types
+val rename_bound_vars_as_displayed :
+  identifier list -> name list -> types -> types
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 688a25b9..a9b2a18b 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pretype_errors.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: pretype_errors.ml 15025 2012-03-09 14:27:07Z glondu $ *)
 
 open Util
 open Stdpp
@@ -45,7 +45,7 @@ exception PretypeError of env * pretype_error
 
 let precatchable_exception = function
   | Util.UserError _ | TypeError _ | PretypeError _
-  | Stdpp.Exc_located(_,(Util.UserError _ | TypeError _ |
+  | Compat.Exc_located(_,(Util.UserError _ | TypeError _ |
     Nametab.GlobalizationError _ | PretypeError _)) -> true
   | _ -> false
 
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index 62941a76..7b09f957 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: typeclasses_errors.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(*i $Id: typeclasses_errors.ml 15025 2012-03-09 14:27:07Z glondu $ i*)
 
 (*i*)
 open Names
@@ -47,7 +47,7 @@ let unsatisfiable_constraints env evd ev =
       raise (TypeClassError (env, UnsatisfiableConstraints (evd, None)))
   | Some ev ->
       let loc, kind = Evd.evar_source ev evd in
-	raise (Stdpp.Exc_located (loc, TypeClassError
+	raise (Compat.Exc_located (loc, TypeClassError
 	  (env, UnsatisfiableConstraints (evd, Some (ev, kind)))))
 
 let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstance (c, n, m))
@@ -55,5 +55,5 @@ let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstan
 let rec unsatisfiable_exception exn =
   match exn with
   | TypeClassError (_, UnsatisfiableConstraints _) -> true
-  | Stdpp.Exc_located(_, e) -> unsatisfiable_exception e
+  | Compat.Exc_located(_, e) -> unsatisfiable_exception e
   | _ -> false
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 395f5c8d..57b183d5 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: vnorm.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(*i $Id: vnorm.ml 15029 2012-03-13 14:47:00Z herbelin $ i*)
 
 open Names
 open Declarations
@@ -111,7 +111,7 @@ let build_branches_type env (mind,_ as _ind) mib mip params dep p =
      a 0) et les lambda correspondant aux realargs *)
   let build_one_branch i cty =
     let typi = type_constructor mind mib cty params in
-    let decl,indapp = Term.decompose_prod typi in
+    let decl,indapp = decompose_prod_assum typi in
     let ind,cargs = find_rectype_a env indapp in
     let nparams = Array.length params in
     let carity = snd (rtbl.(i)) in
@@ -195,11 +195,8 @@ and nf_stk env c t stk  =
       let bsw = branch_of_switch (nb_rel env) sw in
       let mkbranch i (n,v) =
 	let decl,codom = btypes.(i) in
-	let env =
-	  List.fold_right
-	    (fun (name,t) env -> push_rel (name,None,t) env) decl env in
-	let b = nf_val env v codom in
-	compose_lam decl b
+	let b = nf_val (push_rel_context decl env) v codom in
+	it_mkLambda_or_LetIn b decl
       in
       let branchs = Array.mapi mkbranch bsw in
       let tcase = build_case_type dep p realargs c in