From 486acdd7b50d4fdc0956011b7b48dc6ba96dd4a8 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 24 Mar 2017 23:45:54 +0100
Subject: Fix interpretation of Ltac patterns episode 2.

After 5db9588098f9f, some extra evar-normalization remained (compared to trunk)
that would change the semantics e.g. of change bindings under Ltac match.

This is just circumventing a fundamental flaw in the treatment of patterns.
---
 pretyping/patternops.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 8c6b39b7e6..d6a7c5192f 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -153,7 +153,7 @@ 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 (EConstr.to_constr sigma (Retyping.expand_projection env sigma p (EConstr.of_constr c) []))
+      pattern_of_constr env (EConstr.Unsafe.to_constr (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) ->
@@ -218,7 +218,7 @@ let instantiate_pattern env sigma lvar c =
               ctx
           in
 	  let c = substl inst c in
-	  pattern_of_constr env sigma (EConstr.to_constr sigma c)
+	  pattern_of_constr env sigma (EConstr.Unsafe.to_constr c)
 	with Not_found (* List.index failed *) ->
 	  let vars =
 	    List.map_filter (function Name id -> Some id | _ -> None) vars in
-- 
cgit v1.2.3