Merge branch 'v8.5' into trunk

6 files changed, 76 insertions, 48 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 559f5fe66a..055996de55 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -60,9 +60,9 @@ let coe_info_typ_equal c1 c2 =
 
 let cl_typ_ord t1 t2 = match t1, t2 with
   | CL_SECVAR v1, CL_SECVAR v2 -> Id.compare v1 v2
-  | CL_CONST c1, CL_CONST c2 -> con_user_ord c1 c2
-  | CL_PROJ c1, CL_PROJ c2 -> con_user_ord c1 c2
-  | CL_IND i1, CL_IND i2 -> ind_user_ord i1 i2
+  | CL_CONST c1, CL_CONST c2 -> con_ord c1 c2
+  | CL_PROJ c1, CL_PROJ c2 -> con_ord c1 c2
+  | CL_IND i1, CL_IND i2 -> ind_ord i1 i2
   | _ -> Pervasives.compare t1 t2 (** OK *)
 
 module ClTyp = struct
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index cf6ac619dd..161cffa865 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -351,34 +351,45 @@ let authorized_occ env sigma partial_app closed pat c mk_ctx next =
     else mkresult subst (mk_ctx (mkMeta special_meta)) next
   with PatternMatchingFailure -> next ()
 
+let subargs env v = Array.map_to_list (fun c -> (env, c)) v
+
 (* Tries to match a subterm of [c] with [pat] *)
 let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
   let rec aux env c mk_ctx next =
   match kind_of_term c with
   | Cast (c1,k,c2) ->
-      let next_mk_ctx lc = mk_ctx (mkCast (List.hd lc, k,c2)) in
-      let next () = try_aux [env] [c1] next_mk_ctx next in
+      let next_mk_ctx = function
+      | [c1] -> mk_ctx (mkCast (c1, k, c2))
+      | _ -> assert false
+      in
+      let next () = try_aux [env, c1] next_mk_ctx next in
       authorized_occ env sigma partial_app closed pat c mk_ctx next
   | Lambda (x,c1,c2) ->
-      let next_mk_ctx lc = mk_ctx (mkLambda (x,List.hd lc,List.nth lc 1)) in
+      let next_mk_ctx = function
+      | [c1; c2] -> mk_ctx (mkLambda (x, c1, c2))
+      | _ -> assert false
+      in
       let next () = 
 	let env' = Environ.push_rel (x,None,c1) env in
-	  try_aux [env;env'] [c1; c2] next_mk_ctx next in
+        try_aux [(env, c1); (env', c2)] next_mk_ctx next in
       authorized_occ env sigma partial_app closed pat c mk_ctx next
   | Prod (x,c1,c2) ->
-      let next_mk_ctx lc = mk_ctx (mkProd (x,List.hd lc,List.nth lc 1)) in
+      let next_mk_ctx = function
+      | [c1; c2] -> mk_ctx (mkProd (x, c1, c2))
+      | _ -> assert false
+      in
       let next () = 
 	let env' = Environ.push_rel (x,None,c1) env in
-	  try_aux [env;env'] [c1;c2] next_mk_ctx next in
+        try_aux [(env, c1); (env', c2)] next_mk_ctx next in
       authorized_occ env sigma partial_app closed pat c mk_ctx next
   | LetIn (x,c1,t,c2) ->
       let next_mk_ctx = function
-      | [c1;c2] -> mkLetIn (x,c1,t,c2)
+      | [c1; c2] -> mk_ctx (mkLetIn (x, c1, t, c2))
       | _ -> assert false
       in
       let next () = 
 	let env' = Environ.push_rel (x,Some c1,t) env in
-	  try_aux [env;env'] [c1;c2] next_mk_ctx next in
+        try_aux [(env, c1); (env', c2)] next_mk_ctx next in
       authorized_occ env sigma partial_app closed pat c mk_ctx next
   | App (c1,lc) ->
       let next () =
@@ -390,14 +401,15 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
             let mk_ctx = function
               | [app';c] -> mk_ctx (mkApp (app',[|c|]))
               | _ -> assert false in
-            try_aux [env] [app;Array.last lc] mk_ctx next
+            try_aux [(env, app); (env, Array.last lc)] mk_ctx next
           else
             let rec aux2 app args next =
               match args with
               | [] ->
                   let mk_ctx le =
                     mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in
-                  try_aux [env] (c1::Array.to_list lc) mk_ctx next
+                  let sub = (env, c1) :: subargs env lc in
+                  try_aux sub mk_ctx next
               | arg :: args ->
                   let app = mkApp (app,[|arg|]) in
                   let next () = aux2 app args next in
@@ -407,7 +419,8 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
         else
           let mk_ctx le =
             mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in
-          try_aux [env] (c1::Array.to_list lc) mk_ctx next
+          let sub = (env, c1) :: subargs env lc in
+          try_aux sub mk_ctx next
       in
       authorized_occ env sigma partial_app closed pat c mk_ctx next
   | Case (ci,hd,c1,lc) ->
@@ -415,24 +428,24 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
       | [] -> assert false
       | c1 :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc))
       in
-      let next () = try_aux [env] (c1 :: Array.to_list lc) next_mk_ctx next in
+      let sub = (env, c1) :: subargs env lc in
+      let next () = try_aux sub next_mk_ctx next in
       authorized_occ env sigma partial_app closed pat c mk_ctx next
   | Fix (indx,(names,types,bodies)) ->
     let nb_fix = Array.length types in
     let next_mk_ctx le =
       let (ntypes,nbodies) = CList.chop nb_fix le in
       mk_ctx (mkFix (indx,(names, Array.of_list ntypes, Array.of_list nbodies))) in
-    let next () =
-      try_aux
-	[env] ((Array.to_list types)@(Array.to_list bodies)) next_mk_ctx next in
+    let sub = subargs env types @ subargs env bodies in
+    let next () = try_aux sub next_mk_ctx next in
     authorized_occ env sigma partial_app closed pat c mk_ctx next
   | CoFix (i,(names,types,bodies)) ->
     let nb_fix = Array.length types in
     let next_mk_ctx le =
       let (ntypes,nbodies) = CList.chop nb_fix le in
       mk_ctx (mkCoFix (i,(names, Array.of_list ntypes, Array.of_list nbodies))) in
-    let next () =
-      try_aux [env] ((Array.to_list types)@(Array.to_list bodies)) next_mk_ctx next in
+    let sub = subargs env types @ subargs env bodies in
+    let next () = try_aux sub next_mk_ctx next in
     authorized_occ env sigma partial_app closed pat c mk_ctx next
   | Proj (p,c') ->
     let next_mk_ctx le = mk_ctx (mkProj (p,List.hd le)) in
@@ -443,25 +456,22 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
 	    aux env term mk_ctx next
 	with Retyping.RetypeError _ -> next ()
       else
-	try_aux [env] [c'] next_mk_ctx next in
+      try_aux [env, c'] next_mk_ctx next in
       authorized_occ env sigma partial_app closed pat c mk_ctx next
   | Construct _| Ind _|Evar _|Const _ | Rel _|Meta _|Var _|Sort _ ->
       authorized_occ env sigma partial_app closed pat c mk_ctx next
 
   (* Tries [sub_match] for all terms in the list *)
-  and try_aux lenv lc mk_ctx next =
-    let rec try_sub_match_rec lacc lenv lc = 
-      match lenv, lc with
-      | _, [] -> next ()
-      | env :: tlenv, c::tl ->
-          let mk_ctx ce = mk_ctx (List.rev_append lacc (ce::tl)) in
-          let next () = 
-	    let env' = match tlenv with [] -> lenv | _ -> tlenv in
-	      try_sub_match_rec (c::lacc) env' tl 
-	  in
-            aux env c mk_ctx next 
-      | _ -> assert false in
-    try_sub_match_rec [] lenv lc in
+  and try_aux lc mk_ctx next =
+    let rec try_sub_match_rec lacc lc =
+      match lc with
+      | [] -> next ()
+      | (env, c) :: tl ->
+        let mk_ctx ce = mk_ctx (List.rev_append lacc (ce :: List.map snd tl)) in
+        let next () = try_sub_match_rec (c :: lacc) tl in
+        aux env c mk_ctx next
+    in
+    try_sub_match_rec [] lc in
   let lempty () = IStream.Nil in
   let result () = aux env c (fun x -> x) lempty in
   IStream.thunk result
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 67f3cb4169..e514fd529e 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -13,6 +13,9 @@ open Glob_term
 
 val cases_pattern_eq : cases_pattern -> cases_pattern -> bool
 
+val cast_type_eq : ('a -> 'a -> bool) ->
+  'a Misctypes.cast_type -> 'a Misctypes.cast_type -> bool
+
 val glob_constr_eq : glob_constr -> glob_constr -> bool
 
 (** Operations on [glob_constr] *)
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 7f6a4a6442..dfdc24d480 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -365,14 +365,16 @@ let get_arity env ((ind,u),params) =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
   let parsign =
     (* Dynamically detect if called with an instance of recursively
-       uniform parameter only or also of non recursively uniform
+       uniform parameter only or also of recursively non-uniform
        parameters *)
-    let parsign = mib.mind_params_ctxt in
-    let nnonrecparams = mib.mind_nparams - mib.mind_nparams_rec in
-    if Int.equal (List.length params) (rel_context_nhyps parsign - nnonrecparams) then
-      snd (List.chop nnonrecparams mib.mind_params_ctxt)
-    else
-      parsign in
+    let nparams = List.length params in
+    if Int.equal nparams mib.mind_nparams then
+      mib.mind_params_ctxt
+    else begin
+      assert (Int.equal nparams mib.mind_nparams_rec);
+      let nnonrecparamdecls = List.length mib.mind_params_ctxt - mib.mind_nparams_rec in
+      snd (List.chop nnonrecparamdecls mib.mind_params_ctxt)
+    end in
   let parsign = Vars.subst_instance_context u parsign in
   let arproperlength = List.length mip.mind_arity_ctxt - List.length parsign in
   let arsign,_ = List.chop arproperlength mip.mind_arity_ctxt in
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index af1783b705..7959759a3f 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -25,7 +25,9 @@ val type_of_constructors : env -> pinductive -> types array
 (** Return constructor types in normal form *)
 val arities_of_constructors : env -> pinductive -> types array
 
-(** An inductive type with its parameters *)
+(** An inductive type with its parameters (transparently supports
+    reasoning either with only recursively uniform parameters or with all
+    parameters including the recursively non-uniform ones *)
 type inductive_family
 val make_ind_family : inductive puniverses * constr list -> inductive_family
 val dest_ind_family : inductive_family -> inductive puniverses * constr list
@@ -138,10 +140,14 @@ val lift_constructor : int -> constructor_summary -> constructor_summary
 val get_constructor :
   pinductive * mutual_inductive_body * one_inductive_body * constr list ->
   int -> constructor_summary
-val get_arity        : env -> inductive_family -> rel_context * sorts_family
 val get_constructors : env -> inductive_family -> constructor_summary array
 val get_projections  : env -> inductive_family -> constant array option
 
+(** [get_arity] returns the arity of the inductive family instantiated
+    with the parameters; if recursively non-uniform parameters are not
+    part of the inductive family, they appears in the arity *)
+val get_arity        : env -> inductive_family -> rel_context * sorts_family
+
 val build_dependent_constructor : constructor_summary -> constr
 val build_dependent_inductive   : env -> inductive_family -> constr
 val make_arity_signature : env -> bool -> inductive_family -> rel_context
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 19613c4e06..8198db1b8a 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -166,8 +166,15 @@ and nf_whd env whd typ =
       mkApp(cfd,args)
   | Vconstr_const n -> construct_of_constr_const env n typ
   | Vconstr_block b ->
-      let capp,ctyp = construct_of_constr_block env (btag b) typ in
-      let args = nf_bargs env b ctyp in
+      let tag = btag b in
+      let (tag,ofs) =
+        if tag = Cbytecodes.last_variant_tag then
+	  match whd_val (bfield b 0) with
+	  | Vconstr_const tag -> (tag+Cbytecodes.last_variant_tag, 1)
+	  | _ -> assert false
+        else (tag, 0) in
+      let capp,ctyp = construct_of_constr_block env tag typ in
+      let args = nf_bargs env b ofs ctyp in
       mkApp(capp,args)
   | Vatom_stk(Aid idkey, stk) ->
       let c,typ = constr_type_of_idkey env idkey in
@@ -242,14 +249,14 @@ and nf_args env vargs t =
 	t := subst1 c codom; c) in
   !t,args
 
-and nf_bargs env b t =
+and nf_bargs env b ofs t =
   let t = ref t in
-  let len = bsize b in
+  let len = bsize b - ofs in
   let args =
     Array.init len
       (fun i ->
 	let _,dom,codom = decompose_prod env !t in
-	let c = nf_val env (bfield b i) dom in
+	let c = nf_val env (bfield b (i+ofs)) dom in
 	t := subst1 c codom; c) in
   args