Quick hack to fix interpretation of patterns in Ltac.

Interpretation of patterns in Ltac is essentially flawed. It does a roundtrip
through the pretyper, and relies on suspicious flagging of evars in the evar source
field to recognize original pattern holes. After the pattern_of_constr function
was made evar-insensitive, it expanded evars that were solved by magical side-effects
of the pretyper, even if it hadn't been asked to perform any heuristics.

We backtrack on the insensitivity of the pattern_of_constr function. This may have
a performance penalty in other dubious code, e.g. hints. In the long run we should
get rid of the pattern_of_constr function.

1 files changed, 7 insertions, 17 deletions

diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 954aa6a94..823071e29 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -122,10 +122,9 @@ let head_of_constr_reference sigma c = match EConstr.kind sigma c with
   | _ -> anomaly (Pp.str "Not a rigid reference")
 
 let pattern_of_constr env sigma t =
-  let open EConstr in
   let rec pattern_of_constr env t =
   let open Context.Rel.Declaration in
-  match EConstr.kind sigma t with
+  match kind_of_term t with
     | Rel n  -> PRel n
     | Meta n -> PMeta (Some (Id.of_string ("META" ^ string_of_int n)))
     | Var id -> PVar id
@@ -141,7 +140,7 @@ let pattern_of_constr env sigma t =
 				  pattern_of_constr (push_rel (LocalAssum (na, c)) env) b)
     | App (f,a) ->
         (match
-          match EConstr.kind sigma f with
+          match kind_of_term f with
           | Evar (evk,args) ->
             (match snd (Evd.evar_source evk sigma) with
               Evar_kinds.MatchingVar (true,id) -> Some id
@@ -154,18 +153,14 @@ let pattern_of_constr env sigma t =
     | Ind (sp,u)    -> PRef (canonical_gr (IndRef sp))
     | Construct (sp,u) -> PRef (canonical_gr (ConstructRef sp))
     | Proj (p, c) -> 
-      pattern_of_constr env (Retyping.expand_projection env sigma p c [])
+      pattern_of_constr env (EConstr.to_constr sigma (Retyping.expand_projection env sigma p (EConstr.of_constr c) []))
     | Evar (evk,ctxt as ev) ->
       (match snd (Evd.evar_source evk sigma) with
       | Evar_kinds.MatchingVar (b,id) ->
-	let ty = existential_type sigma ev in
-	let () = ignore (pattern_of_constr env ty) in
         assert (not b); PMeta (Some id)
       | Evar_kinds.GoalEvar -> 
 	PEvar (evk,Array.map (pattern_of_constr env) ctxt)
       | _ -> 
-	let ty = existential_type sigma ev in
-	let () = ignore (pattern_of_constr env ty) in
 	 PMeta None)
     | Case (ci,p,a,br) ->
         let cip =
@@ -179,13 +174,8 @@ let pattern_of_constr env sigma t =
 	in
 	PCase (cip, pattern_of_constr env p, pattern_of_constr env a,
 	       Array.to_list (Array.mapi branch_of_constr br))
-    | Fix (idx, (nas, cs, ts)) ->
-      let inj c = EConstr.to_constr sigma c in
-      PFix (idx, (nas, Array.map inj cs, Array.map inj ts))
-    | CoFix (idx, (nas, cs, ts)) ->
-      let inj c = EConstr.to_constr sigma c in
-      PCoFix (idx, (nas, Array.map inj cs, Array.map inj ts))
-  in
+    | Fix f -> PFix f
+    | CoFix f -> PCoFix f in
   pattern_of_constr env t
 
 (* To process patterns, we need a translation without typing at all. *)
@@ -228,7 +218,7 @@ let instantiate_pattern env sigma lvar c =
               ctx
           in
 	  let c = substl inst c in
-	  pattern_of_constr env sigma c
+	  pattern_of_constr env sigma (EConstr.to_constr sigma c)
 	with Not_found (* List.index failed *) ->
 	  let vars =
 	    List.map_filter (function Name id -> Some id | _ -> None) vars in
@@ -253,7 +243,7 @@ let rec subst_pattern subst pat =
   | PRef ref ->
       let ref',t = subst_global subst ref in
 	if ref' == ref then pat else
-	 pattern_of_constr (Global.env()) Evd.empty (EConstr.of_constr t)
+	 pattern_of_constr (Global.env()) Evd.empty t
   | PVar _
   | PEvar _
   | PRel _ -> pat