1 files changed, 78 insertions, 19 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index e5294715..613581ad 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -23,7 +23,6 @@ open Typing
 open Proof_type
 open Type_errors
 open Retyping
-open Misctypes
 
 module NamedDecl = Context.Named.Declaration
 
@@ -63,6 +62,7 @@ let is_unification_error = function
 
 let catchable_exception = function
   | CErrors.UserError _ | TypeError _
+  | Notation.NumeralNotationError _
   | RefinerError _ | Indrec.RecursionSchemeError _
   | Nametab.GlobalizationError _
   (* reduction errors *)
@@ -185,6 +185,22 @@ let check_decl_position env sigma sign d =
  * on the right side [right] if [toleft=false].
  * If [with_dep] then dependent hypotheses are moved accordingly. *)
 
+(** Move destination for hypothesis *)
+
+type 'id move_location =
+  | MoveAfter of 'id
+  | MoveBefore of 'id
+  | MoveFirst
+  | MoveLast (** can be seen as "no move" when doing intro *)
+
+(** Printing of [move_location] *)
+
+let pr_move_location pr_id = function
+  | MoveAfter id -> brk(1,1) ++ str "after " ++ pr_id id
+  | MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id
+  | MoveFirst -> str " at top"
+  | MoveLast -> str " at bottom"
+
 let move_location_eq m1 m2 = match m1, m2 with
 | MoveAfter id1, MoveAfter id2 -> Id.equal id1 id2
 | MoveBefore id1, MoveBefore id2 -> Id.equal id1 id2
@@ -236,7 +252,7 @@ let move_hyp sigma toleft (left,declfrom,right) hto =
 	      (first, d::middle)
             else
 	      user_err ~hdr:"move_hyp" (str "Cannot move " ++ Id.print (NamedDecl.get_id declfrom) ++
-	        Miscprint.pr_move_location Id.print hto ++
+                pr_move_location Id.print hto ++
 	        str (if toleft then ": it occurs in the type of " else ": it depends on ")
 	        ++ Id.print hyp ++ str ".")
           else
@@ -289,7 +305,15 @@ let collect_meta_variables c =
   let rec collrec deep acc c = match kind c with
     | Meta mv -> if deep then error_unsupported_deep_meta () else mv::acc
     | Cast(c,_,_) -> collrec deep acc c
-    | (App _| Case _) -> Constr.fold (collrec deep) acc c
+    | Case(ci,p,c,br) ->
+        (* Hack assuming only two situations: the legacy one that branches,
+           if with Metas, are Meta, and the new one with eta-let-expanded
+           branches *)
+        let br = Array.map2 (fun n b -> try snd (Term.decompose_lam_n_decls n b) with UserError _ -> b) ci.ci_cstr_ndecls br in
+        Array.fold_left (collrec deep)
+          (Constr.fold (collrec deep) (Constr.fold (collrec deep) acc p) c)
+          br
+    | App _ -> Constr.fold (collrec deep) acc c
     | Proj (_, c) -> collrec deep acc c
     | _ -> Constr.fold (collrec true) acc c
   in
@@ -301,9 +325,10 @@ let check_meta_variables env sigma c =
 
 let check_conv_leq_goal env sigma arg ty conclty =
   if !check then
-    let evm, b = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in
-      if b then evm 
-      else raise (RefinerError (env, sigma, BadType (arg,ty,conclty)))
+    let ans = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in
+    match ans with
+    | Some evm -> evm
+    | None -> raise (RefinerError (env, sigma, BadType (arg,ty,conclty)))
   else sigma
 
 exception Stop of EConstr.t list
@@ -387,12 +412,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
       | Case (ci,p,c,lf) ->
 	let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals sigma goal goalacc p c in
 	let sigma = check_conv_leq_goal env sigma trm conclty' conclty in
-	let (acc'',sigma, rbranches) =
-	  Array.fold_left2
-            (fun (lacc,sigma,bacc) ty fi ->
-	       let (r,_,s,b') = mk_refgoals sigma goal lacc ty fi in r,s,(b'::bacc))
-            (acc',sigma,[]) lbrty lf
-	in
+        let (acc'',sigma,rbranches) = treat_case sigma goal ci lbrty lf acc' in
         let lf' = Array.rev_of_list rbranches in
         let ans =
           if p' == p && c' == c && Array.equal (==) lf' lf then trm
@@ -440,12 +460,7 @@ and mk_hdgoals sigma goal goalacc trm =
 
     | Case (ci,p,c,lf) ->
 	let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals sigma goal goalacc p c in
-	let (acc'',sigma,rbranches) =
-	  Array.fold_left2
-            (fun (lacc,sigma,bacc) ty fi ->
-	       let (r,_,s,b') = mk_refgoals sigma goal lacc ty fi in r,s,(b'::bacc))
-            (acc',sigma,[]) lbrty lf
-	in
+        let (acc'',sigma,rbranches) = treat_case sigma goal ci lbrty lf acc' in
 	let lf' = Array.rev_of_list rbranches in
 	let ans =
           if p' == p && c' == c && Array.equal (==) lf' lf then trm
@@ -483,7 +498,7 @@ and mk_arggoals sigma goal goalacc funty allargs =
       let env = Goal.V82.env sigma goal in
       raise (RefinerError (env,sigma,CannotApply (t, harg)))
   in
-  Array.smartfoldmap foldmap (goalacc, funty, sigma) allargs
+  Array.Smart.fold_left_map foldmap (goalacc, funty, sigma) allargs
 
 and mk_casegoals sigma goal goalacc p c =
   let env = Goal.V82.env sigma goal in
@@ -497,6 +512,50 @@ and mk_casegoals sigma goal goalacc p c =
   let (lbrty,conclty) = type_case_branches_with_names env sigma indspec p c in
   (acc'',lbrty,conclty,sigma,p',c')
 
+and treat_case sigma goal ci lbrty lf acc' =
+  let rec strip_outer_cast c = match kind c with
+  | Cast (c,_,_) -> strip_outer_cast c
+  | _ -> c in
+  let decompose_app_vect c = match kind c with
+  | App (f,cl) -> (f, cl)
+  | _ -> (c,[||]) in
+  let env = Goal.V82.env sigma goal in
+  Array.fold_left3
+    (fun (lacc,sigma,bacc) ty fi l ->
+        if isMeta (strip_outer_cast fi) then
+          (* Support for non-eta-let-expanded Meta as found in *)
+          (* destruct/case with an non eta-let expanded elimination scheme *)
+          let (r,_,s,fi') = mk_refgoals sigma goal lacc ty fi in
+          r,s,(fi'::bacc)
+        else
+        (* Deal with a branch in expanded form of the form
+           Case(ci,p,c,[|eta-let-exp(Meta);...;eta-let-exp(Meta)|]) as
+           if it were not so, so as to preserve compatibility with when
+           destruct/case generated schemes of the form
+           Case(ci,p,c,[|Meta;...;Meta|];
+           CAUTION: it does not deal with the general case of eta-zeta
+           reduced branches having a form different from Meta, as it
+           would be theoretically the case with third-party code *)
+        let n = List.length l in
+        let ctx, body = Term.decompose_lam_n_decls n fi in
+        let head, args = decompose_app_vect body in
+        (* Strip cast because clenv_cast_meta adds a cast when the branch is
+           eta-expanded but when not when the branch has the single-meta
+           form [Meta] *)
+        let head = strip_outer_cast head in
+        if isMeta head then begin
+          assert (args = Context.Rel.to_extended_vect mkRel 0 ctx);
+          let head' = lift (-n) head in
+          let (r,_,s,head'') = mk_refgoals sigma goal lacc ty head' in
+          let fi' = it_mkLambda_or_LetIn (mkApp (head'',args)) ctx in
+          (r,s,fi'::bacc)
+        end
+        else
+          (* Supposed to be meta-free *)
+          let sigma, t'ty = goal_type_of env sigma fi in
+          let sigma = check_conv_leq_goal env sigma fi t'ty ty in
+          (lacc,sigma,fi::bacc))
+    (acc',sigma,[]) lbrty lf ci.ci_pp_info.cstr_tags
 
 let convert_hyp check sign sigma d =
   let id = NamedDecl.get_id d in