From caa033a1b998279fd1c98798210d44a7032c2ef6 Mon Sep 17 00:00:00 2001
From: barras
Date: Wed, 2 Jun 2004 12:01:04 +0000
Subject: bug #787 de Roland

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

diff --git a/tactics/refine.ml b/tactics/refine.ml
index 20621b8e0a..036554937c 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -184,10 +184,10 @@ let rec compute_metamap env gmm c = match kind_of_term c with
 	  TH (c,[],[])
       end
 
-  | Case (ci,p,c,v) ->
+  | Case (ci,p,cc,v) ->
       (* bof... *)
       let nbr = Array.length v in
-      let v = Array.append [|p;c|] v in
+      let v = Array.append [|p;cc|] v in
       let a = Array.map (compute_metamap env gmm) v in
       begin
 	try
-- 
cgit v1.2.3