Merge branch 'v8.5'

6 files changed, 33 insertions, 11 deletions

diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 161cffa865..e281807131 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -428,7 +428,7 @@ 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 sub = (env, c1) :: subargs env lc in
+      let sub = (env, hd) :: (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)) ->
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index f388f90057..97b1b16455 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -201,13 +201,6 @@ let ise_and evd l =
 	| UnifFailure _ as x -> x in
   ise_and evd l
 
-(* This function requires to get the outermost arguments first.  It is
-   a fold_right for backward compatibility.
-
-   It tries to unify the suffix of 2 lists element by element and if
-   it reaches the end of a list, it returns the remaining elements in
-   the other list if there are some.
-*)
 let ise_exact ise x1 x2 =
   match ise x1 x2 with
   | None, out -> out
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 201a16ebeb..2508f4ef3b 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -844,6 +844,25 @@ let subterm_source evk (loc,k) =
   (loc,Evar_kinds.SubEvar evk)
 
 
-(** Term exploration up to isntantiation. *)
+(** Term exploration up to instantiation. *)
 let kind_of_term_upto sigma t =
   Constr.kind (Reductionops.whd_evar sigma t)
+
+(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and
+    [u] up to existential variable instantiation and equalisable
+    universes. The term [t] is interpreted in [sigma1] while [u] is
+    interpreted in [sigma2]. The universe constraints in [sigma2] are
+    assumed to be an extention of those in [sigma1]. *)
+let eq_constr_univs_test sigma1 sigma2 t u =
+  (* spiwack: mild code duplication with {!Evd.eq_constr_univs}. *)
+  let open Evd in
+  let b, c =
+    Universes.eq_constr_univs_infer_with
+      (fun t -> kind_of_term_upto sigma1 t)
+      (fun u -> kind_of_term_upto sigma2 u)
+      (universes sigma2) t u
+  in
+  if b then
+    try let _ = add_universe_constraints sigma2 c in true
+    with Univ.UniverseInconsistency _ | UniversesDiffer -> false
+  else false
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 49036798e6..f1d94b0a4f 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -206,6 +206,13 @@ val flush_and_check_evars :  evar_map -> constr -> constr
     value of [e] in [sigma] is (recursively) used. *)
 val kind_of_term_upto : evar_map -> constr -> (constr,types) kind_of_term
 
+(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and
+    [u] up to existential variable instantiation and equalisable
+    universes. The term [t] is interpreted in [sigma1] while [u] is
+    interpreted in [sigma2]. The universe constraints in [sigma2] are
+    assumed to be an extention of those in [sigma1]. *)
+val eq_constr_univs_test : evar_map -> evar_map -> constr -> constr -> bool
+
 (** {6 debug pretty-printer:} *)
 
 val pr_tycon : env -> type_constraint -> Pp.std_ppcmds
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 705e594af1..fb629d049f 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -395,7 +395,9 @@ let rec pat_of_raw metas vars = function
 	| Some p, Some (_,_,nal) ->
           let nvars = na :: List.rev nal @ vars in
           rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas nvars p))
-	| _ -> PMeta None
+        | (None | Some (GHole _)), _ -> PMeta None
+	| Some p, None ->
+            user_err_loc (loc,"",strbrk "Clause \"in\" expected in patterns over \"match\" expressions with an explicit \"return\" clause.")
       in
       let info =
 	{ cip_style = sty;
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 01e1154e58..c2281e13a5 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1528,7 +1528,8 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
     let ids = ids_of_named_context (named_context env) in
     if name == Anonymous then next_ident_away_in_goal x ids else
     if mem_named_context x (named_context env) then
-      error ("The variable "^(Id.to_string x)^" is already declared.")
+      errorlabstrm "Unification.make_abstraction_core"
+        (str "The variable " ++ Nameops.pr_id x ++ str " is already declared.")
     else
       x
   in