Merge remote-tracking branch 'upstream/trunk' into trunk

17 files changed, 427 insertions, 147 deletions

diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index 1bd03491a7..c7b37aba5c 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -43,7 +43,7 @@ let section_segment_of_reference = function
   | ConstRef con -> Lib.section_segment_of_constant con
   | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
       Lib.section_segment_of_mutual_inductive kn
-  | _ -> [], Univ.LMap.empty, Univ.UContext.empty
+  | _ -> [], Univ.LMap.empty, Univ.AUContext.empty
 
 let discharge_rename_args = function
   | _, (ReqGlobal (c, names), _ as req) ->
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index c3f392980a..b88532e1b9 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -245,6 +245,7 @@ let push_history_pattern n pci cont =
 
 type 'a pattern_matching_problem =
     { env       : env;
+      lvar      : Glob_term.ltac_var_map;
       evdref    : evar_map ref;
       pred      : constr;
       tomatch   : tomatch_stack;
@@ -346,25 +347,45 @@ let find_tomatch_tycon evdref env loc = function
   | None ->
       empty_tycon,None
 
-let coerce_row typing_fun evdref env pats (tomatch,(_,indopt)) =
+let make_return_predicate_ltac_lvar sigma na tm c lvar =
+  match na, tm.CAst.v with
+  | Name id, (GVar id' | GRef (Globnames.VarRef id', _)) when Id.equal id id' ->
+     if Id.Map.mem id lvar.ltac_genargs then
+       let ltac_genargs = Id.Map.remove id lvar.ltac_genargs in
+       let ltac_idents = match kind sigma c with
+       | Var id' -> Id.Map.add id id' lvar.ltac_idents
+       | _ -> lvar.ltac_idents in
+       { lvar with ltac_genargs; ltac_idents }
+     else lvar
+  | _ -> lvar
+
+let ltac_interp_realnames lvar = function
+  | t, IsInd (ty,ind,realnal) -> t, IsInd (ty,ind,List.map (ltac_interp_name lvar) realnal)
+  | _ as x -> x
+
+let coerce_row typing_fun evdref env lvar pats (tomatch,(na,indopt)) =
   let loc = loc_of_glob_constr tomatch in
   let tycon,realnames = find_tomatch_tycon evdref env loc indopt in
-  let j = typing_fun tycon env evdref tomatch in
+  let j = typing_fun tycon env evdref !lvar tomatch in
   let evd, j = Coercion.inh_coerce_to_base ?loc:(loc_of_glob_constr tomatch) env !evdref j in
   evdref := evd;
   let typ = nf_evar !evdref j.uj_type in
+  lvar := make_return_predicate_ltac_lvar !evdref na tomatch j.uj_val !lvar;
   let t =
     try try_find_ind env !evdref typ realnames
     with Not_found ->
       unify_tomatch_with_patterns evdref env loc typ pats realnames in
   (j.uj_val,t)
 
-let coerce_to_indtype typing_fun evdref env matx tomatchl = 
+let coerce_to_indtype typing_fun evdref env lvar matx tomatchl =
   let pats = List.map (fun r ->  r.patterns) matx in
   let matx' = match matrix_transpose pats with
     | [] -> List.map (fun _ -> []) tomatchl (* no patterns at all *)
     | m -> m in
-  List.map2 (coerce_row typing_fun evdref env) matx' tomatchl
+  let lvar = ref lvar in
+  let tms = List.map2 (coerce_row typing_fun evdref env lvar) matx' tomatchl in
+  let tms = List.map (ltac_interp_realnames !lvar) tms in
+  !lvar,tms
 
 (************************************************************************)
 (* Utils *)
@@ -1392,6 +1413,7 @@ and match_current pb (initial,tomatch) =
             postprocess_dependencies !(pb.evdref) depstocheck
               brvals pb.tomatch pb.pred deps cstrs in
           let brvals = Array.map (fun (sign,body) ->
+            let sign = List.map (map_name (ltac_interp_name pb.lvar)) sign in
             it_mkLambda_or_LetIn body sign) brvals in
 	  let (pred,typ) =
 	    find_predicate pb.caseloc pb.env pb.evdref
@@ -1824,6 +1846,7 @@ let build_inversion_problem loc env sigma tms t =
   let evdref = ref sigma in
   let pb =
     { env       = pb_env;
+      lvar      = empty_lvar;
       evdref    = evdref;
       pred      = (*ty *) mkSort s;
       tomatch   = sub_tms;
@@ -1847,15 +1870,15 @@ let build_initial_predicate arsign pred =
     | _ -> assert false
   in buildrec 0 pred [] (List.rev arsign)
 
-let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
+let extract_arity_signature ?(dolift=true) env0 lvar tomatchl tmsign =
   let lift = if dolift then lift else fun n t -> t in
   let get_one_sign n tm (na,t) =
     match tm with
       | NotInd (bo,typ) ->
 	  (match t with
-	    | None -> (match bo with
+	    | None -> let sign = match bo with
 		       | None -> [LocalAssum (na, lift n typ)]
-		       | Some b -> [LocalDef (na, lift n b, lift n typ)])
+		       | Some b -> [LocalDef (na, lift n b, lift n typ)] in sign,sign
 	    | Some (loc,_) ->
  	    user_err ?loc 
                 (str"Unexpected type annotation for a term of non inductive type."))
@@ -1865,22 +1888,31 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
 	  let nrealargs_ctxt = inductive_nrealdecls_env env0 ind in
 	  let arsign = fst (get_arity env0 indf') in
 	  let arsign = List.map (fun d -> map_rel_decl EConstr.of_constr d) arsign in
-	  let realnal =
+	  let realnal, realnal' =
 	    match t with
 	      | Some (loc,(ind',realnal)) ->
 		  if not (eq_ind ind ind') then
 		    user_err ?loc  (str "Wrong inductive type.");
 		  if not (Int.equal nrealargs_ctxt (List.length realnal)) then
 		      anomaly (Pp.str "Ill-formed 'in' clause in cases.");
-		  List.rev realnal
-	      | None -> List.make nrealargs_ctxt Anonymous in
-	  LocalAssum (na, EConstr.of_constr (build_dependent_inductive env0 indf'))
-	  ::(List.map2 RelDecl.set_name realnal arsign) in
+		  let realnal = List.rev realnal in
+                  let realnal' = List.map (ltac_interp_name lvar) realnal in
+                  realnal,realnal'
+	      | None ->
+                  let realnal = List.make nrealargs_ctxt Anonymous in
+                  realnal, realnal in
+          let na' = ltac_interp_name lvar na in
+          let t = EConstr.of_constr (build_dependent_inductive env0 indf') in
+          (* Context with names for typing *)
+          let arsign1 = LocalAssum (na, t) :: List.map2 RelDecl.set_name realnal arsign in
+          (* Context with names for building the term *)
+          let arsign2 = LocalAssum (na', t) :: List.map2 RelDecl.set_name realnal' arsign in
+          arsign1,arsign2 in
   let rec buildrec n = function
     | [],[] -> []
     | (_,tm)::ltm, (_,x)::tmsign ->
 	let l = get_one_sign n tm x in
-	l :: buildrec (n + List.length l) (ltm,tmsign)
+	l :: buildrec (n + List.length (fst l)) (ltm,tmsign)
     | _ -> assert false
   in List.rev (buildrec 0 (tomatchl,tmsign))
 
@@ -1970,7 +2002,7 @@ let noccur_with_meta sigma n m term =
   in
   try (occur_rec n term; true) with LocalOccur -> false
 
-let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred =
+let prepare_predicate ?loc typing_fun env sigma lvar tomatchs arsign tycon pred =
   let refresh_tycon sigma t =
     (** If we put the typing constraint in the term, it has to be
        refreshed to preserve the invariant that no algebraic universe
@@ -1978,6 +2010,7 @@ let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred =
     refresh_universes ~status:Evd.univ_flexible ~onlyalg:true (Some true)
 		      env sigma t
   in
+  let typing_arsign,building_arsign = List.split arsign in
   let preds =
     match pred, tycon with
     (* No return clause *)
@@ -1987,7 +2020,7 @@ let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred =
        (* First strategy: we abstract the tycon wrt to the dependencies *)
          let sigma, t = refresh_tycon sigma t in
          let p1 =
-          prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign t in
+          prepare_predicate_from_arsign_tycon env sigma loc tomatchs typing_arsign t in
 	(* Second strategy: we build an "inversion" predicate *)
 	let sigma2,pred2 = build_inversion_problem loc env sigma tomatchs t in
 	(match p1 with
@@ -2006,22 +2039,22 @@ let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred =
         (* First strategy: we build an "inversion" predicate *)
 	let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in
 	(* Second strategy: we directly use the evar as a non dependent pred *)
-        let pred2 = lift (List.length (List.flatten arsign)) t in
+        let pred2 = lift (List.length (List.flatten typing_arsign)) t in
 	[sigma1, pred1; sigma, pred2]
     (* Some type annotation *)
     | Some rtntyp, _ ->
       (* We extract the signature of the arity *)
-      let envar = List.fold_right push_rel_context arsign env in
+      let envar = List.fold_right push_rel_context typing_arsign env in
       let sigma, newt = new_sort_variable univ_flexible_alg sigma in
       let evdref = ref sigma in
-      let predcclj = typing_fun (mk_tycon (mkSort newt)) envar evdref rtntyp in
+      let predcclj = typing_fun (mk_tycon (mkSort newt)) envar evdref lvar rtntyp in
       let sigma = !evdref in
       let predccl = nf_evar sigma predcclj.uj_val in
       [sigma, predccl]
   in
   List.map
     (fun (sigma,pred) ->
-      let (nal,pred) = build_initial_predicate arsign pred in
+      let (nal,pred) = build_initial_predicate building_arsign pred in
       sigma,nal,pred)
     preds
 
@@ -2441,10 +2474,10 @@ let context_of_arsign l =
     l ([], 0)
   in x
 
-let compile_program_cases ?loc style (typing_function, evdref) tycon env
+let compile_program_cases ?loc style (typing_function, evdref) tycon env lvar
     (predopt, tomatchl, eqns) =
   let typing_fun tycon env = function
-    | Some t ->	typing_function tycon env evdref t
+    | Some t ->	typing_function tycon env evdref lvar t
     | None -> Evarutil.evd_comb0 use_unit_judge evdref in
 
   (* We build the matrix of patterns and right-hand side *)
@@ -2452,14 +2485,15 @@ let compile_program_cases ?loc style (typing_function, evdref) tycon env
 
   (* We build the vector of terms to match consistently with the *)
   (* constructors found in patterns *)
-  let tomatchs = coerce_to_indtype typing_function evdref env matx tomatchl in
+  let predlvar,tomatchs = coerce_to_indtype typing_function evdref env lvar matx tomatchl in
   let tycon = valcon_of_tycon tycon in
   let tomatchs, tomatchs_lets, tycon' = abstract_tomatch env !evdref tomatchs tycon in
   let env = push_rel_context tomatchs_lets env in
   let len = List.length eqns in
   let sign, allnames, signlen, eqs, neqs, args =
     (* The arity signature *)
-    let arsign = extract_arity_signature ~dolift:false env tomatchs tomatchl in
+    let arsign = extract_arity_signature ~dolift:false env predlvar tomatchs tomatchl in
+    let arsign = List.map fst arsign in (* Because no difference between the arity for typing and the arity for building *)
       (* Build the dependent arity signature, the equalities which makes
 	 the first part of the predicate and their instantiations. *)
     let avoid = [] in
@@ -2522,11 +2556,12 @@ let compile_program_cases ?loc style (typing_function, evdref) tycon env
   let initial_pushed = List.map (fun x -> Pushed (true,x)) typs' in
     
   let typing_function tycon env evdref = function
-    | Some t ->	typing_function tycon env evdref t
+    | Some t ->	typing_function tycon env evdref lvar t
     | None -> evd_comb0 use_unit_judge evdref in
 
   let pb =
     { env      = env;
+      lvar     = lvar;
       evdref   = evdref;
       pred     = pred;
       tomatch  = initial_pushed;
@@ -2548,10 +2583,10 @@ let compile_program_cases ?loc style (typing_function, evdref) tycon env
 (**************************************************************************)
 (* Main entry of the matching compilation                                 *)
 
-let compile_cases ?loc style (typing_fun, evdref) tycon env (predopt, tomatchl, eqns) =
+let compile_cases ?loc style (typing_fun, evdref) tycon env lvar (predopt, tomatchl, eqns) =
   if predopt == None && Flags.is_program_mode () && Program.is_program_cases () then
     compile_program_cases ?loc style (typing_fun, evdref)
-      tycon env (predopt, tomatchl, eqns)
+      tycon env lvar (predopt, tomatchl, eqns)
   else
 
   (* We build the matrix of patterns and right-hand side *)
@@ -2559,15 +2594,15 @@ let compile_cases ?loc style (typing_fun, evdref) tycon env (predopt, tomatchl,
 
   (* We build the vector of terms to match consistently with the *)
   (* constructors found in patterns *)
-  let tomatchs = coerce_to_indtype typing_fun evdref env matx tomatchl in
+  let predlvar,tomatchs = coerce_to_indtype typing_fun evdref env lvar matx tomatchl in
 
 
 
   (* If an elimination predicate is provided, we check it is compatible
      with the type of arguments to match; if none is provided, we
      build alternative possible predicates *)
-  let arsign = extract_arity_signature env tomatchs tomatchl in
-  let preds = prepare_predicate ?loc typing_fun env !evdref tomatchs arsign tycon predopt in
+  let arsign = extract_arity_signature env predlvar tomatchs tomatchl in
+  let preds = prepare_predicate ?loc typing_fun env !evdref predlvar tomatchs arsign tycon predopt in
 
   let compile_for_one_predicate (sigma,nal,pred) =
     (* We push the initial terms to match and push their alias to rhs' envs *)
@@ -2598,13 +2633,14 @@ let compile_cases ?loc style (typing_fun, evdref) tycon env (predopt, tomatchl,
 
     (* A typing function that provides with a canonical term for absurd cases*)
     let typing_fun tycon env evdref = function
-    | Some t ->	typing_fun tycon env evdref t
+    | Some t ->	typing_fun tycon env evdref lvar t
     | None -> evd_comb0 use_unit_judge evdref in
 
     let myevdref = ref sigma in
 
     let pb =
       { env       = env;
+        lvar      = lvar;
         evdref    = myevdref;
 	pred      = pred;
 	tomatch   = initial_pushed;
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index b16342db4b..4b1fde25a8 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -39,9 +39,9 @@ val irrefutable : env -> cases_pattern -> bool
 
 val compile_cases :
   ?loc:Loc.t -> case_style ->
-  (type_constraint -> env -> evar_map ref -> glob_constr -> unsafe_judgment) * evar_map ref ->
+  (type_constraint -> env -> evar_map ref -> ltac_var_map -> glob_constr -> unsafe_judgment) * evar_map ref ->
   type_constraint ->
-  env -> glob_constr option * tomatch_tuples * cases_clauses ->
+  env -> ltac_var_map -> glob_constr option * tomatch_tuples * cases_clauses ->
   unsafe_judgment
 
 val constr_of_pat : 
@@ -101,6 +101,7 @@ and pattern_continuation =
 
 type 'a pattern_matching_problem =
     { env       : env;
+      lvar      : Glob_term.ltac_var_map;
       evdref    : evar_map ref;
       pred      : constr;
       tomatch   : tomatch_stack;
@@ -115,10 +116,14 @@ val compile : 'a pattern_matching_problem -> unsafe_judgment
 
 val prepare_predicate : ?loc:Loc.t ->
            (Evarutil.type_constraint ->
-            Environ.env -> Evd.evar_map ref -> glob_constr -> unsafe_judgment) ->
+            Environ.env -> Evd.evar_map ref -> ltac_var_map -> glob_constr -> unsafe_judgment) ->
            Environ.env ->
            Evd.evar_map ->
+           Glob_term.ltac_var_map ->
            (types * tomatch_type) list ->
-           rel_context list ->
+           (rel_context * rel_context) list ->
            constr option ->
            glob_constr option -> (Evd.evar_map * Names.name list * constr) list
+
+val make_return_predicate_ltac_lvar : Evd.evar_map -> Names.name ->
+  Glob_term.glob_constr -> constr -> Glob_term.ltac_var_map -> Glob_term.ltac_var_map
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 9a973cff55..8d87f6e99c 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -428,7 +428,7 @@ let automatically_import_coercions = ref false
 open Goptions
 let _ =
   declare_bool_option
-    { optdepr  = false;
+    { optdepr  = true; (* remove in 8.8 *)
       optname  = "automatic import of coercions";
       optkey   = ["Automatic";"Coercions";"Import"];
       optread  = (fun () -> !automatically_import_coercions);
@@ -454,15 +454,11 @@ let cache_coercion (_, c) =
   add_coercion_in_graph (xf,is,it)
 
 let load_coercion _ o =
-  if
-    !automatically_import_coercions || Flags.version_less_or_equal Flags.V8_2
-  then
+  if !automatically_import_coercions then
     cache_coercion o
 
 let open_coercion i o =
-  if Int.equal i 1 && not
-    (!automatically_import_coercions || Flags.version_less_or_equal Flags.V8_2)
-  then
+  if Int.equal i 1 && not !automatically_import_coercions then
     cache_coercion o
 
 let subst_coercion (subst, c) =
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 3757ba7e6d..d84363089d 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -350,6 +350,26 @@ let exact_ise_stack2 env evd f sk1 sk2 =
     ise_stack2 evd (List.rev sk1) (List.rev sk2)
   else UnifFailure (evd, (* Dummy *) NotSameHead)
 
+let check_leq_inductives evd cumi u u' =
+  let u = EConstr.EInstance.kind evd u in
+  let u' = EConstr.EInstance.kind evd u' in
+  let length_ind_instance = 
+    Univ.Instance.length
+      (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi))
+  in
+  let ind_sbcst =  Univ.ACumulativityInfo.subtyp_context cumi in
+  if not ((length_ind_instance = Univ.Instance.length u) &&
+          (length_ind_instance = Univ.Instance.length u')) then
+     anomaly (Pp.str "Invalid inductive subtyping encountered!")
+  else
+    begin
+     let comp_subst = (Univ.Instance.append u u') in
+     let comp_cst = 
+       Univ.UContext.constraints (Univ.subst_instance_context comp_subst ind_sbcst)
+     in
+     Evd.add_constraints evd comp_cst
+    end
+
 let rec evar_conv_x ts env evd pbty term1 term2 =
   let term1 = whd_head_evar evd term1 in
   let term2 = whd_head_evar evd term2 in
@@ -439,16 +459,102 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
     else evar_eqappr_x ts env' evd CONV out2 out1
   in
   let rigids env evd sk term sk' term' =
-    let univs = EConstr.eq_constr_universes evd term term' in
-    match univs with
-    | Some univs ->
-       ise_and evd [(fun i ->
-         let cstrs = Universes.to_constraints (Evd.universes i) univs in
-           try Success (Evd.add_constraints i cstrs)
-           with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p));
-                  (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk sk')]
-    | None ->
-      UnifFailure (evd,NotSameHead)
+    let check_strict () =
+      let univs = EConstr.eq_constr_universes evd term term' in
+      match univs with
+      | Some univs ->
+        begin
+          let cstrs = Universes.to_constraints (Evd.universes evd) univs in
+          try Success (Evd.add_constraints evd cstrs)
+          with Univ.UniverseInconsistency p -> UnifFailure (evd, UnifUnivInconsistency p)
+        end
+      | None ->
+        UnifFailure (evd, NotSameHead)
+    in
+    let first_try_strict_check cond u u' try_subtyping_constraints =
+      if cond then
+        let univs = EConstr.eq_constr_universes evd term term' in
+        match univs with
+        | Some univs ->
+          begin
+            let cstrs = Universes.to_constraints (Evd.universes evd) univs in
+            try Success (Evd.add_constraints evd cstrs)
+            with Univ.UniverseInconsistency p -> try_subtyping_constraints ()
+          end
+        | None ->
+          UnifFailure (evd, NotSameHead)
+      else
+        UnifFailure (evd, NotSameHead)
+    in
+    let compare_heads evd = 
+      match EConstr.kind evd term, EConstr.kind evd term' with
+      | Const (c, u), Const (c', u') ->
+        check_strict ()
+      | Ind (ind, u), Ind (ind', u') ->
+        let check_subtyping_constraints () =
+          let nparamsaplied = Stack.args_size sk in
+          let nparamsaplied' = Stack.args_size sk' in
+          begin
+            let mind = Environ.lookup_mind (fst ind) env in
+            match mind.Declarations.mind_universes with
+            | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
+              UnifFailure (evd, NotSameHead)
+            | Declarations.Cumulative_ind cumi ->
+              begin
+                let num_param_arity =
+                  mind.Declarations.mind_nparams + 
+                  mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs
+                in
+                if not (num_param_arity = nparamsaplied
+                        && num_param_arity = nparamsaplied') then
+                  UnifFailure (evd, NotSameHead)
+                else
+                  begin
+                    let evd' = check_leq_inductives evd cumi u u' in
+                    Success (check_leq_inductives evd' cumi u' u)
+                  end
+              end
+          end
+        in
+        first_try_strict_check (Names.eq_ind ind ind') u u' check_subtyping_constraints
+      | Construct (cons, u), Construct (cons', u') ->
+        let check_subtyping_constraints () =
+          let ind, ind' = fst cons, fst cons' in
+          let j, j' = snd cons, snd cons' in
+          let nparamsaplied = Stack.args_size sk in
+          let nparamsaplied' = Stack.args_size sk' in
+          let mind = Environ.lookup_mind (fst ind) env in
+          match mind.Declarations.mind_universes with
+          | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
+            UnifFailure (evd, NotSameHead)
+          | Declarations.Cumulative_ind cumi ->
+            begin
+              let num_cnstr_args =
+                let nparamsctxt =
+                  mind.Declarations.mind_nparams + 
+                  mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs
+                in
+                nparamsctxt + 
+                mind.Declarations.mind_packets.(snd ind).
+                  Declarations.mind_consnrealargs.(j - 1)
+              in
+              if not (num_cnstr_args = nparamsaplied 
+                      && num_cnstr_args = nparamsaplied') then
+                UnifFailure (evd, NotSameHead)
+              else
+                begin
+                  let evd' = check_leq_inductives evd cumi u u' in
+                  Success (check_leq_inductives evd' cumi u' u)
+                end
+            end
+        in
+        first_try_strict_check (Names.eq_constructor cons cons') u u' check_subtyping_constraints
+      | _, _ -> anomaly (Pp.str "")
+    in
+    ise_and evd [(fun i ->
+                try compare_heads i
+                with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p));
+                 (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk sk')]
   in
   let flex_maybeflex on_left ev ((termF,skF as apprF),cstsF) ((termM, skM as apprM),cstsM) vM =
     let switch f a b = if on_left then f a b else f b a in
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 62ff9ac708..9c09396ccc 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -504,3 +504,27 @@ let glob_constr_of_closed_cases_pattern = function
       na,glob_constr_of_closed_cases_pattern_aux (CAst.make ?loc @@ PatCstr (cstr,l,Anonymous))
   | _ ->
       raise Not_found
+
+(**********************************************************************)
+(* Interpreting ltac variables *)
+
+open Pp
+open CErrors
+
+let ltac_interp_name { ltac_idents ; ltac_genargs } = function
+  | Anonymous -> Anonymous
+  | Name id as n ->
+      try Name (Id.Map.find id ltac_idents)
+      with Not_found ->
+        if Id.Map.mem id ltac_genargs then
+          user_err (str"Ltac variable"++spc()++ pr_id id ++
+                           spc()++str"is not bound to an identifier."++spc()++
+                           str"It cannot be used in a binder.")
+        else n
+
+let empty_lvar : ltac_var_map = {
+  ltac_constrs = Id.Map.empty;
+  ltac_uconstrs = Id.Map.empty;
+  ltac_idents = Id.Map.empty;
+  ltac_genargs = Id.Map.empty;
+}
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 75db04f77f..6bb421e732 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -83,3 +83,6 @@ val cases_pattern_of_glob_constr : Name.t -> glob_constr -> cases_pattern
 val glob_constr_of_closed_cases_pattern : cases_pattern -> Name.t * glob_constr
 
 val add_patterns_for_params_remove_local_defs : constructor -> cases_pattern list -> cases_pattern list
+
+val ltac_interp_name : Glob_term.ltac_var_map -> Names.name -> Names.name
+val empty_lvar : Glob_term.ltac_var_map
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index d8252ea9bb..2ae7c0f809 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -655,3 +655,93 @@ let control_only_guard env c =
     iter_constr_with_full_binders push_rel iter env c
   in
   iter env c
+
+(* inference of subtyping condition for inductive types *)
+
+let infer_inductive_subtyping_arity_constructor
+    (env, evd, csts) (subst : constr -> constr) (arcn : Term.types) is_arity (params : Context.Rel.t) =
+  let numchecked = ref 0 in
+  let numparams = Context.Rel.nhyps params in
+  let update_contexts (env, evd, csts) csts' =
+    (Environ.add_constraints csts' env, Evd.add_constraints evd csts', Univ.Constraint.union csts csts')
+  in
+  let basic_check (env, evd, csts) tp =
+    let result =
+      if !numchecked >= numparams then
+        let csts' =
+          Reduction.infer_conv_leq ~evars:(Evd.existential_opt_value evd) env (Evd.universes evd) tp (subst tp)
+        in update_contexts (env, evd, csts) csts'
+      else
+        (env, evd, csts)
+    in
+    numchecked := !numchecked + 1; result
+  in
+  let infer_typ typ ctxs =
+   match typ with
+     | LocalAssum (_, typ') ->
+       begin
+         try
+           let (env, evd, csts) = basic_check ctxs typ' in (Environ.push_rel typ env, evd, csts)
+         with Reduction.NotConvertible -> 
+           anomaly ~label:"inference of record/inductive subtyping relation failed"
+             (Pp.str "Can't infer subtyping for record/inductive type")
+       end
+     | _ -> anomaly (Pp.str "")
+  in
+  let arcn' = Term.it_mkProd_or_LetIn arcn params in
+  let typs, codom = Reduction.dest_prod env arcn' in
+  let last_contexts = Context.Rel.fold_outside infer_typ typs ~init:(env, evd, csts) in
+  if not is_arity then basic_check last_contexts codom else last_contexts
+
+let infer_inductive_subtyping env evd mind_ent =
+  let { Entries.mind_entry_params = params;
+        Entries.mind_entry_inds = entries;
+        Entries.mind_entry_universes = ground_univs;
+      } = mind_ent
+  in
+  let uinfind =
+    match ground_univs with
+    | Entries.Monomorphic_ind_entry _
+    | Entries.Polymorphic_ind_entry _ -> ground_univs
+    | Entries.Cumulative_ind_entry cumi -> 
+      begin
+        let uctx = Univ.CumulativityInfo.univ_context cumi in
+        let sbsubst = Univ.CumulativityInfo.subtyping_susbst cumi in
+        let dosubst = subst_univs_level_constr sbsubst in
+        let instance_other = 
+          Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) 
+        in
+        let constraints_other = 
+          Univ.subst_univs_level_constraints
+            sbsubst (Univ.UContext.constraints uctx) 
+        in
+        let uctx_other = Univ.UContext.make (instance_other, constraints_other) in
+        let env = Environ.push_context uctx env in
+        let env = Environ.push_context uctx_other env in
+        let evd = 
+          Evd.merge_universe_context
+            evd (UState.of_context_set (Univ.ContextSet.of_context uctx_other)) 
+        in
+        let (_, _, subtyp_constraints) =
+          List.fold_left
+            (fun ctxs indentry ->
+               let _, params = Typeops.infer_local_decls env params in
+               let ctxs' = infer_inductive_subtyping_arity_constructor
+                   ctxs dosubst indentry.Entries.mind_entry_arity true params
+               in
+               List.fold_left
+                 (fun ctxs cons ->
+                    infer_inductive_subtyping_arity_constructor
+                      ctxs dosubst cons false params
+                 )
+                 ctxs' indentry.Entries.mind_entry_lc
+            ) (env, evd, Univ.Constraint.empty) entries
+        in 
+        Entries.Cumulative_ind_entry
+          (Univ.CumulativityInfo.make 
+             (Univ.CumulativityInfo.univ_context cumi,
+              Univ.UContext.make
+                (Univ.UContext.instance (Univ.CumulativityInfo.subtyp_context cumi),
+                 subtyp_constraints)))
+      end
+  in {mind_ent with Entries.mind_entry_universes = uinfind;}
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index bdb6f996b9..811f47f39a 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -199,3 +199,12 @@ val type_of_inductive_knowing_conclusion :
 
 (********************)
 val control_only_guard : env -> types -> unit
+
+(* inference of subtyping condition for inductive types *)
+(* for debugging purposes only to be removed *)
+val infer_inductive_subtyping_arity_constructor : Environ.env * Evd.evar_map * Univ.Constraint.t ->
+(Term.constr -> Term.constr) ->
+Term.types -> bool -> Context.Rel.t -> Environ.env * Evd.evar_map * Univ.Constraint.t
+
+val infer_inductive_subtyping : Environ.env -> Evd.evar_map -> Entries.mutual_inductive_entry ->
+  Entries.mutual_inductive_entry
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 92e728683d..7488f35bfe 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -42,21 +42,11 @@ open Pretype_errors
 open Glob_term
 open Glob_ops
 open Evarconv
-open Pattern
 open Misctypes
 
 module NamedDecl = Context.Named.Declaration
 
 type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
-type var_map = constr_under_binders Id.Map.t
-type uconstr_var_map = Glob_term.closed_glob_constr Id.Map.t
-type unbound_ltac_var_map = Geninterp.Val.t Id.Map.t
-type ltac_var_map = {
-  ltac_constrs : var_map;
-  ltac_uconstrs : uconstr_var_map;
-  ltac_idents: Id.t Id.Map.t;
-  ltac_genargs : unbound_ltac_var_map;
-}
 type glob_constr_ltac_closure = ltac_var_map * glob_constr
 type pure_open_constr = evar_map * EConstr.constr
 
@@ -419,17 +409,6 @@ let orelse_name name name' = match name with
   | Anonymous -> name'
   | _ -> name
 
-let ltac_interp_name { ltac_idents ; ltac_genargs } = function
-  | Anonymous -> Anonymous
-  | Name id as n ->
-      try Name (Id.Map.find id ltac_idents)
-      with Not_found ->
-        if Id.Map.mem id ltac_genargs then
-          user_err  (str"Ltac variable"++spc()++ pr_id id ++
-                           spc()++str"is not bound to an identifier."++spc()++
-                           str"It cannot be used in a binder.")
-        else n
-
 let ltac_interp_name_env k0 lvar env sigma =
   (* envhd is the initial part of the env when pretype was called first *)
   (* (in practice is is probably 0, but we have to grant the
@@ -943,16 +922,20 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	  List.map (set_name Anonymous) arsgn
 	else arsgn
     in
-      let psign = LocalAssum (na, build_dependent_inductive env.ExtraEnv.env indf) :: arsgn in
+      let indt = build_dependent_inductive env.ExtraEnv.env indf in
+      let psign = LocalAssum (na, indt) :: arsgn in (* For locating names in [po] *)
+      let predlvar = Cases.make_return_predicate_ltac_lvar !evdref na c cj.uj_val lvar in
+      let psign' = LocalAssum (ltac_interp_name predlvar na, indt) :: arsgn in
+      let psign' = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign' in
+      let psign' = Namegen.name_context env.ExtraEnv.env !evdref psign' in (* For naming abstractions in [po] *)
       let psign = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign in
       let nar = List.length arsgn in
 	  (match po with
 	  | Some p ->
 	    let env_p = push_rel_context !evdref psign env in
-	    let pj = pretype_type empty_valcon env_p evdref lvar p in
+	    let pj = pretype_type empty_valcon env_p evdref predlvar p in
 	    let ccl = nf_evar !evdref pj.utj_val in
-	    let psign = make_arity_signature env.ExtraEnv.env !evdref true indf in (* with names *)
-	    let p = it_mkLambda_or_LetIn ccl psign in
+	    let p = it_mkLambda_or_LetIn ccl psign' in
 	    let inst =
 	      (Array.map_to_list EConstr.of_constr cs.cs_concl_realargs)
 	      @[EConstr.of_constr (build_dependent_constructor cs)] in
@@ -968,7 +951,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 
 	  | None ->
 	    let tycon = lift_tycon cs.cs_nargs tycon in
-	    let fj = pretype tycon env_f evdref lvar d in
+	    let fj = pretype tycon env_f evdref predlvar d in
 	    let ccl = nf_evar !evdref fj.uj_type in
 	    let ccl =
 	      if noccur_between !evdref 1 cs.cs_nargs ccl then
@@ -977,7 +960,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 		error_cant_find_case_type ?loc env.ExtraEnv.env !evdref
 		  cj.uj_val in
 		 (* let ccl = refresh_universes ccl in *)
-	    let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
+	    let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign' in
 	    let v =
 	      let ind,_ = dest_ind_family indf in
 		Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val p;
@@ -1004,14 +987,19 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	  else arsgn
       in
       let nar = List.length arsgn in
-      let psign = LocalAssum (na, build_dependent_inductive env.ExtraEnv.env indf) :: arsgn in
+      let indt = build_dependent_inductive env.ExtraEnv.env indf in
+      let psign = LocalAssum (na, indt) :: arsgn in (* For locating names in [po] *)
+      let predlvar = Cases.make_return_predicate_ltac_lvar !evdref na c cj.uj_val lvar in
+      let psign' = LocalAssum (ltac_interp_name predlvar na, indt) :: arsgn in
+      let psign' = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign' in
+      let psign' = Namegen.name_context env.ExtraEnv.env !evdref psign' in (* For naming abstractions in [po] *)
       let psign = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign in
       let pred,p = match po with
 	| Some p ->
 	  let env_p = push_rel_context !evdref psign env in
-	  let pj = pretype_type empty_valcon env_p evdref lvar p in
+	  let pj = pretype_type empty_valcon env_p evdref predlvar p in
 	  let ccl = nf_evar !evdref pj.utj_val in
-	  let pred = it_mkLambda_or_LetIn ccl psign in
+	  let pred = it_mkLambda_or_LetIn ccl psign' in
 	  let typ = lift (- nar) (beta_applist !evdref (pred,[cj.uj_val])) in
 	    pred, typ
 	| None ->
@@ -1021,7 +1009,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
               let env = ltac_interp_name_env k0 lvar env !evdref in
               new_type_evar env evdref loc
 	  in
-	    it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
+	    it_mkLambda_or_LetIn (lift (nar+1) p) psign', p in
       let pred = nf_evar !evdref pred in
       let p = nf_evar !evdref p in
       let f cs b =
@@ -1054,8 +1042,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 
   | GCases (sty,po,tml,eqns) ->
     Cases.compile_cases ?loc sty
-      ((fun vtyc env evdref -> pretype vtyc (make_env env !evdref) evdref lvar),evdref)
-      tycon env.ExtraEnv.env (* loc *) (po,tml,eqns)
+      ((fun vtyc env evdref -> pretype vtyc (make_env env !evdref) evdref),evdref)
+      tycon env.ExtraEnv.env (* loc *) lvar (po,tml,eqns)
 
   | GCast (c,k) ->
     let cj =
@@ -1198,13 +1186,6 @@ let no_classes_no_fail_inference_flags = {
 let all_and_fail_flags = default_inference_flags true
 let all_no_fail_flags = default_inference_flags false
 
-let empty_lvar : ltac_var_map = {
-  ltac_constrs = Id.Map.empty;
-  ltac_uconstrs = Id.Map.empty;
-  ltac_idents = Id.Map.empty;
-  ltac_genargs = Id.Map.empty;
-}
-
 let on_judgment sigma f j =
   let c = mkCast(j.uj_val,DEFAULTcast, j.uj_type) in
   let (c,_,t) = destCast sigma (f c) in
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index dcacd07209..e17468ef83 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -12,7 +12,6 @@
    into elementary ones, insertion of coercions and resolution of
    implicit arguments. *)
 
-open Names
 open Term
 open Environ
 open Evd
@@ -28,23 +27,6 @@ val search_guard :
 
 type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
 
-type var_map = Pattern.constr_under_binders Id.Map.t
-type uconstr_var_map = Glob_term.closed_glob_constr Id.Map.t
-type unbound_ltac_var_map = Geninterp.Val.t Id.Map.t
-
-type ltac_var_map = {
-  ltac_constrs : var_map;
-  (** Ltac variables bound to constrs *)
-  ltac_uconstrs : uconstr_var_map;
-  (** Ltac variables bound to untyped constrs *)
-  ltac_idents: Id.t Id.Map.t;
-  (** Ltac variables bound to identifiers *)
-  ltac_genargs : unbound_ltac_var_map;
-  (** Ltac variables bound to other kinds of arguments *)
-}
-
-val empty_lvar : ltac_var_map
-
 type glob_constr_ltac_closure = ltac_var_map * glob_constr
 type pure_open_constr = evar_map * constr
 
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index bc9e3a1f46..283a1dcd18 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -197,7 +197,7 @@ let warn_projection_no_head_constant =
 (* Intended to always succeed *)
 let compute_canonical_projections warn (con,ind) =
   let env = Global.env () in
-  let ctx = Univ.instantiate_univ_context (Environ.constant_context env con) in
+  let ctx = Environ.constant_context env con in
   let u = Univ.UContext.instance ctx in
   let v = (mkConstU (con,u)) in
   let ctx = Univ.ContextSet.of_context ctx in
@@ -298,8 +298,7 @@ let error_not_structure ref =
 let check_and_decompose_canonical_structure ref =
   let sp = match ref with ConstRef sp -> sp | _ -> error_not_structure ref in
   let env = Global.env () in
-  let ctx = Environ.constant_context env sp in
-  let u = Univ.UContext.instance ctx in
+  let u = Environ.constant_instance env sp in
   let vc = match Environ.constant_opt_value_in env (sp, u) with
     | Some vc -> vc
     | None -> error_not_structure ref in
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index c2a6483012..123c610166 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1313,8 +1313,8 @@ let pb_equal = function
   | Reduction.CUMUL -> Reduction.CONV
   | Reduction.CONV -> Reduction.CONV
 
-let report_anomaly _ =
-  let e = UserError (None, Pp.str "Conversion test raised an anomaly") in
+let report_anomaly e =
+  let e = UserError (None, Pp.(str "Conversion test raised an anomaly" ++ print e)) in
   let e = CErrors.push e in
   iraise e
 
@@ -1361,9 +1361,81 @@ let sigma_compare_instances ~flex i0 i1 sigma =
      | Univ.UniverseInconsistency _ ->
 	raise Reduction.NotConvertible
 
+let sigma_check_inductive_instances cv_pb uinfind u u' sigma =
+  let ind_instance = 
+    Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context uinfind) 
+  in
+  let ind_sbctx =  Univ.ACumulativityInfo.subtyp_context uinfind  in
+  if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) &&
+          (Univ.Instance.length ind_instance = Univ.Instance.length u')) then
+     anomaly (Pp.str "Invalid inductive subtyping encountered!")
+  else
+    let comp_cst =
+      let comp_subst = (Univ.Instance.append u u') in
+      Univ.UContext.constraints (Univ.subst_instance_context comp_subst ind_sbctx)
+    in
+    let comp_cst =
+      match cv_pb with
+        Reduction.CONV -> 
+        let comp_subst = (Univ.Instance.append u' u) in
+        let comp_cst' = 
+          Univ.UContext.constraints(Univ.subst_instance_context comp_subst ind_sbctx)
+        in
+        Univ.Constraint.union comp_cst comp_cst'
+      | Reduction.CUMUL -> comp_cst
+    in
+    try Evd.add_constraints sigma comp_cst
+    with Evd.UniversesDiffer
+       | Univ.UniverseInconsistency _ ->
+      raise Reduction.NotConvertible
+
+let sigma_conv_inductives
+    cv_pb (mind, ind) u1 sv1 u2 sv2 sigma =
+  try sigma_compare_instances ~flex:false u1 u2 sigma with
+    Reduction.NotConvertible ->
+    match mind.Declarations.mind_universes with
+    | Declarations.Monomorphic_ind _ ->
+      raise Reduction.NotConvertible
+    | Declarations.Polymorphic_ind _ ->
+      raise Reduction.NotConvertible
+    | Declarations.Cumulative_ind cumi ->
+      let num_param_arity =
+        mind.Declarations.mind_nparams + 
+        mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
+      in
+      if not (num_param_arity = sv1 && num_param_arity = sv2) then
+        raise Reduction.NotConvertible
+      else
+        sigma_check_inductive_instances cv_pb cumi u1 u2 sigma 
+
+let sigma_conv_constructors
+    (mind, ind, cns) u1 sv1 u2 sv2 sigma =
+  try sigma_compare_instances ~flex:false u1 u2 sigma with
+    Reduction.NotConvertible ->
+    match mind.Declarations.mind_universes with
+    | Declarations.Monomorphic_ind _ ->
+      raise Reduction.NotConvertible
+    | Declarations.Polymorphic_ind _ ->
+      raise Reduction.NotConvertible
+    | Declarations.Cumulative_ind cumi ->
+      let num_cnstr_args =
+        let nparamsctxt =
+          mind.Declarations.mind_nparams + 
+          mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
+        in
+        nparamsctxt + 
+        mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(cns - 1)
+      in
+      if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then
+        raise Reduction.NotConvertible
+      else
+        sigma_check_inductive_instances Reduction.CONV cumi u1 u2 sigma
+
 let sigma_univ_state = 
   { Reduction.compare = sigma_compare_sorts;
-    Reduction.compare_instances = sigma_compare_instances }
+    Reduction.compare_instances = sigma_compare_instances;
+    Reduction.conv_inductives = sigma_conv_inductives;
+    Reduction.conv_constructors = sigma_conv_constructors}
 
 let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL)
     ?(ts=full_transparent_state) env sigma x y =
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index af4ea3ac53..a4da19de75 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -66,7 +66,6 @@ module Cst_stack : sig
   val pr : t -> Pp.std_ppcmds
 end
 
-
 module Stack : sig
   type 'a app_node
 
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index d7b4842810..f883e647b5 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -111,20 +111,16 @@ let new_instance cl info glob poly impl =
 let classes : typeclasses ref = Summary.ref Refmap.empty ~name:"classes"
 let instances : instances ref = Summary.ref Refmap.empty ~name:"instances"
 
-open Declarations
-
 let typeclass_univ_instance (cl,u') =
   let subst = 
     let u = 
       match cl.cl_impl with
       | ConstRef c -> 
         let cb = Global.lookup_constant c in
-	  if cb.const_polymorphic then Univ.UContext.instance cb.const_universes
-	  else Univ.Instance.empty
+        Declareops.constant_polymorphic_instance cb
       | IndRef c ->
          let mib,oib = Global.lookup_inductive c in
-	  if mib.mind_polymorphic then Univ.UContext.instance mib.mind_universes
-	  else Univ.Instance.empty
+         Declareops.inductive_polymorphic_instance mib
       | _ -> Univ.Instance.empty
     in Array.fold_left2 (fun subst u u' -> Univ.LMap.add u u' subst) 
       Univ.LMap.empty (Univ.Instance.to_array u) (Univ.Instance.to_array u')
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 0fb48ed8cf..67c8b07e78 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -248,24 +248,13 @@ let sort_eqns = unify_r2l
 
 let global_pattern_unification_flag = ref true
 
-(* Compatibility option introduced and activated in Coq 8.3 whose
-   syntax is now deprecated. *)
-
 open Goptions
-let _ =
-  declare_bool_option
-    { optdepr  = true;
-      optname  = "pattern-unification for existential variables in tactics";
-      optkey   = ["Tactic";"Evars";"Pattern";"Unification"];
-      optread  = (fun () -> !global_pattern_unification_flag);
-      optwrite = (:=) global_pattern_unification_flag }
 
-(* Compatibility option superseding the previous one, introduced and
-   activated in Coq 8.4 *)
+(* Compatibility option introduced and activated in Coq 8.4 *)
 
 let _ =
   declare_bool_option
-    { optdepr  = false;
+    { optdepr  = true; (* remove in 8.8 *)
       optname  = "pattern-unification for existential variables in tactics";
       optkey   = ["Tactic";"Pattern";"Unification"];
       optread  = (fun () -> !global_pattern_unification_flag);
@@ -481,12 +470,10 @@ let set_flags_for_type flags = { flags with
 
 let use_evars_pattern_unification flags =
   !global_pattern_unification_flag && flags.use_pattern_unification
-  && Flags.version_strictly_greater Flags.V8_2
 
 let use_metas_pattern_unification sigma flags nb l =
   !global_pattern_unification_flag && flags.use_pattern_unification
-  || (Flags.version_less_or_equal Flags.V8_3 || 
-      flags.use_meta_bound_pattern_unification) &&
+  || flags.use_meta_bound_pattern_unification &&
      Array.for_all (fun c -> isRel sigma c && destRel sigma c <= nb) l
 
 type key = 
@@ -609,9 +596,6 @@ let do_reduce ts (env, nb) sigma c =
   Stack.zip sigma (fst (whd_betaiota_deltazeta_for_iota_state
 		  ts env sigma Cst_stack.empty (c, Stack.empty)))
 
-let use_full_betaiota flags =
-  flags.modulo_betaiota && Flags.version_strictly_greater Flags.V8_3
-
 let isAllowedEvar sigma flags c = match EConstr.kind sigma c with
   | Evar (evk,_) -> not (Evar.Set.mem evk flags.frozen_evars)
   | _ -> false
@@ -949,7 +933,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
 	  expand curenvnb pb opt substn cM f1 l1 cN f2 l2
 
   and reduce curenvnb pb opt (sigma, metas, evars as substn) cM cN =
-    if use_full_betaiota flags && not (subterm_restriction opt flags) then
+    if flags.modulo_betaiota && not (subterm_restriction opt flags) then
       let cM' = do_reduce flags.modulo_delta curenvnb sigma cM in
 	if not (EConstr.eq_constr sigma cM cM') then
 	  unirec_rec curenvnb pb opt substn cM' cN
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index b08666483e..9e151fea25 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -174,8 +174,7 @@ and nf_whd env sigma whd typ =
   | Vatom_stk(Aind ((mi,i) as ind), stk) ->
      let mib = Environ.lookup_mind mi env in
      let nb_univs =
-       if mib.mind_polymorphic then Univ.UContext.size mib.mind_universes
-       else 0
+       Univ.Instance.length (Declareops.inductive_polymorphic_instance mib)
      in
      let mk u =
        let pind = (ind, u) in (mkIndU pind, type_of_ind env pind)
@@ -204,8 +203,7 @@ and constr_type_of_idkey env sigma (idkey : Vars.id_key) stk =
   | ConstKey cst ->
      let cbody = Environ.lookup_constant cst env in
      let nb_univs =
-       if cbody.const_polymorphic then Univ.UContext.size cbody.const_universes
-       else 0
+       Univ.Instance.length (Declareops.constant_polymorphic_instance cbody)
      in
      let mk u =
        let pcst = (cst, u) in (mkConstU pcst, Typeops.type_of_constant_in env pcst)