diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/refine.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/tactics/refine.ml b/tactics/refine.ml index 8ec991c0f1..6c87782fcc 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -213,8 +213,7 @@ let rec compute_metamap env c = match kind_of_term c with TH (c,[],[]) (* Autres cas. *) - | IsXtra _|IsCoFix _ -> - invalid_arg "Tcc.compute_metamap" + | IsCoFix _ -> invalid_arg "Tcc.compute_metamap" (* tcc_aux : term_with_holes -> tactic |