diff options
Diffstat (limited to 'pretyping/tacred.ml')
| -rw-r--r-- | pretyping/tacred.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 02524f896..3fc01c86c 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1148,7 +1148,6 @@ let compute = cbv_betadeltaiota let abstract_scheme env sigma (locc,a) (c, sigma) = let ta = Retyping.get_type_of env sigma a in - let ta = EConstr.of_constr ta in let na = named_hd env (EConstr.to_constr sigma ta) Anonymous in if occur_meta sigma ta then error "Cannot find a type for the generalisation."; if occur_meta sigma a then |