diff options
| -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 |