diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-01-30 04:21:51 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-01-30 04:21:51 +0000 |
| commit | 2b9f73c7e86ac718c0ce4c47d6a24ffc2d01499d (patch) | |
| tree | 4036fe3c992e406c790d165b17424c3530653277 /contrib/subtac/subtac_pretyping_F.ml | |
| parent | 90b063be6b3c23a54e1d59974e09ee14f2941338 (diff) | |
Work on dependent induction tactic and friends, finish the test-suite example
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10487 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/subtac/subtac_pretyping_F.ml')
| -rw-r--r-- | contrib/subtac/subtac_pretyping_F.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml index 36a0e9c91..986825f25 100644 --- a/contrib/subtac/subtac_pretyping_F.ml +++ b/contrib/subtac/subtac_pretyping_F.ml @@ -566,8 +566,6 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct (pretype_type empty_valcon env isevars lvar c).utj_val in let evd,_ = consider_remaining_unif_problems env !isevars in let evd = nf_evar_defs evd in - let c' = nf_evar (evars_of evd) c' in -(* let evd = undefined_evars evd in *) let evd = Typeclasses.resolve_typeclasses env (evars_of evd) evd in let c' = nf_evar (evars_of evd) c' in isevars := evd; |