diff options
| author | barras | 2004-06-02 12:01:04 +0000 |
|---|---|---|
| committer | barras | 2004-06-02 12:01:04 +0000 |
| commit | caa033a1b998279fd1c98798210d44a7032c2ef6 (patch) | |
| tree | c220000cd559ce0e00a86030009f28f318d0973d | |
| parent | 92bcea3d77e14de97759b59efb3b4edc8da4a715 (diff) | |
bug #787 de Roland
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5783 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/refine.ml | 4 |
1 files 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 |