diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-02-19 10:14:14 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-02-19 10:14:14 +0000 |
| commit | baecd07714a5ed44c3b288e73e2b41367b880db1 (patch) | |
| tree | 541df9f2a6eab12414bdbac0065cf36482254d7e /contrib/subtac/subtac_pretyping_F.ml | |
| parent | 40a716f91bc6c6ee05bcca0fefa38857991317c8 (diff) | |
Various little subtac fixes, add some useful tactics.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9659 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, 1 insertions, 1 deletions
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml index dc199c1d0..e53dad265 100644 --- a/contrib/subtac/subtac_pretyping_F.ml +++ b/contrib/subtac/subtac_pretyping_F.ml @@ -93,7 +93,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct (* coerce to tycon if any *) let inh_conv_coerce_to_tycon loc env isevars j = function - | None -> j + | None -> j_nf_isevar !isevars j | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) isevars j t let push_rels vars env = List.fold_right push_rel vars env |