From f5458f9064be5cc4f645019df6519b265281a280 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 28 Jun 2010 07:27:28 +0000
Subject: Fixed a bug introduced in a combination in r12807 and revealed in
 r13080 via a failure in CoRN (pattern_of_constr needs correct sigma).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13205 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/pattern.ml  | 4 ++--
 pretyping/pattern.mli | 2 +-
 tactics/tacinterp.ml  | 2 +-
 3 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 59f3cde88a..fd51f7952f 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -163,7 +163,7 @@ let error_instantiate_pattern id l =
     ++ strbrk " in pattern because the term refers to " ++ pr_enum pr_id l
     ++ strbrk " which " ++ str is ++ strbrk " not bound in the pattern.")
 
-let instantiate_pattern lvar c =
+let instantiate_pattern sigma lvar c =
   let rec aux vars = function
   | PVar id as x ->
       (try
@@ -172,7 +172,7 @@ let instantiate_pattern lvar c =
 	  let inst =
 	    List.map (fun id -> mkRel (list_index (Name id) vars)) ctx in
 	  let c = substl inst c in
-	  snd (pattern_of_constr Evd.empty c)
+	  snd (pattern_of_constr sigma c)
 	with Not_found (* list_index failed *) ->
 	  let vars =
 	    list_map_filter (function Name id -> Some id | _ -> None) vars in
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index 5685f3d2c5..344a6239b8 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -111,7 +111,7 @@ val pattern_of_rawconstr : rawconstr ->
       patvar list * constr_pattern
 
 val instantiate_pattern :
-  (identifier * (identifier list * constr)) list ->
+  Evd.evar_map -> (identifier * (identifier list * constr)) list ->
   constr_pattern -> constr_pattern
 
 val lift_pattern : int -> constr_pattern -> constr_pattern
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 04ef9befb1..5230ff810c 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1667,7 +1667,7 @@ let eval_pattern lfun ist env sigma (_,pat as c) =
   if use_types then
     snd (interp_typed_pattern ist env sigma c)
   else
-    instantiate_pattern lfun pat
+    instantiate_pattern sigma lfun pat
 
 let read_pattern lfun ist env sigma = function
   | Subterm (b,ido,c) -> Subterm (b,ido,eval_pattern lfun ist env sigma c)
-- 
cgit v1.2.3