From 685ae9ecd6635ab4e44368f8eb2c7415e6de42f6 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 5 Oct 2011 15:52:07 +0000
Subject: When a pattern match, don't use the first matching term but an
 instance of the initial pattern (this fixes compilation of CoRN after
 r14499).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14516 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tactics.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 957d2c4764..2f0eaf82e0 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1704,18 +1704,18 @@ let default_matching_flags sigma = {
 let make_pattern_test env sigma0 (sigma,c) =
   let flags = default_matching_flags sigma0 in
   let matching_fun t =
-    try ignore (w_unify env Reduction.CONV ~flags c t sigma); Some t
+    try let sigma = w_unify env Reduction.CONV ~flags c t sigma in Some(sigma,t)
     with _ -> raise NotUnifiable in
   let merge_fun c1 c2 =
     match c1, c2 with
-    | Some c1, Some c2 when not (is_fconv Reduction.CONV env sigma0 c1 c2) ->
+    | Some (_,c1), Some (_,c2) when not (is_fconv Reduction.CONV env sigma0 c1 c2) ->
         raise NotUnifiable
     | _ -> c1 in
   { match_fun = matching_fun; merge_fun = merge_fun; 
     testing_state = None; last_found = None },
   (fun test -> match test.testing_state with
    | None -> finish_evar_resolution env sigma0 (sigma,c)
-   | Some c -> c)
+   | Some (sigma,_) -> nf_evar sigma c)
 
 let letin_abstract id c (test,out) (occs,check_occs) gl =
   let env = pf_env gl in
-- 
cgit v1.2.3