Posssible abstractions over goal variables when inferring match return clause.

The no-inversion and maximal abstraction over dependencies now
supports abstraction over goal variables rather than only on "rel"
variables. In particular, it now works consistently using
"intro H; refine (match H with ... end)" or
"refine (fun H => match H with ... end)".

By doing so, we ensure that all three strategies are tried in all
situations where a return clause has to be inferred, even in the
context of a "refine".

See antepenultimate commit for discussion.

1 files changed, 25 insertions, 11 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 1b1f95883..e89c3ea71 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1870,16 +1870,22 @@ let inh_conv_coerce_to_tycon loc env evdref j tycon =
 
 (* We put the tycon inside the arity signature, possibly discovering dependencies. *)
 
+let add_subst c len (rel_subst,var_subst) =
+  match kind_of_term c with
+  | Rel n -> (n,len) :: rel_subst, var_subst
+  | Var id -> rel_subst, (id,len) :: var_subst
+  | _ -> assert false
+
 let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
   let nar = List.fold_left (fun n sign -> Context.Rel.nhyps sign + n) 0 arsign in
-  let subst, len =
+  let (rel_subst,var_subst), len =
     List.fold_right2 (fun (tm, tmtype) sign (subst, len) ->
       let signlen = List.length sign in
 	match kind_of_term tm with
-	  | Rel n when dependent tm c
+	  | Rel _ | Var _ when dependent tm c
 		&& Int.equal signlen 1 (* The term to match is not of a dependent type itself *) ->
-	      ((n, len) :: subst, len - signlen)
-	  | Rel n when signlen > 1 (* The term is of a dependent type,
+	      (add_subst tm len subst, len - signlen)
+	  | Rel _ | Var _ when signlen > 1 (* The term is of a dependent type,
 				      maybe some variable in its type appears in the tycon. *) ->
 	      (match tmtype with
 		  NotInd _ -> (subst, len - signlen)
@@ -1888,28 +1894,36 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
 		      List.fold_left
 			(fun (subst, len) arg ->
 			  match kind_of_term arg with
-			  | Rel n when dependent arg c ->
-			      ((n, len) :: subst, pred len)
+			  | Rel _ | Var _ when dependent arg c ->
+			      (add_subst arg len subst, pred len)
 			  | _ -> (subst, pred len))
 			(subst, len) realargs
 		    in
 		    let subst =
-		      if dependent tm c && List.for_all isRel realargs
-		      then (n, len) :: subst else subst
+		      if dependent tm c && List.for_all (fun c -> isRel c || isVar c) realargs
+		      then add_subst tm len subst else subst
 		    in (subst, pred len))
 	  | _ -> (subst, len - signlen))
-      (List.rev tomatchs) arsign ([], nar)
+      (List.rev tomatchs) arsign (([],[]), nar)
   in
   let rec predicate lift c =
     match kind_of_term c with
       | Rel n when n > lift ->
 	  (try
 	      (* Make the predicate dependent on the matched variable *)
-	      let idx = Int.List.assoc (n - lift) subst in
+	      let idx = Int.List.assoc (n - lift) rel_subst in
 		mkRel (idx + lift)
 	    with Not_found ->
-	      (* A variable that is not matched, lift over the arsign. *)
+	      (* A variable that is not matched, lift over the arsign *)
 	      mkRel (n + nar))
+      | Var id ->
+	  (try
+	      (* Make the predicate dependent on the matched variable *)
+	      let idx = Id.List.assoc id var_subst in
+		mkRel (idx + lift)
+	    with Not_found ->
+	      (* A variable that is not matched *)
+	      c)
       | _ ->
 	  map_constr_with_binders succ predicate lift c
   in