diff options
| author | msozeau | 2007-02-19 10:14:14 +0000 |
|---|---|---|
| committer | msozeau | 2007-02-19 10:14:14 +0000 |
| commit | baecd07714a5ed44c3b288e73e2b41367b880db1 (patch) | |
| tree | 541df9f2a6eab12414bdbac0065cf36482254d7e /contrib/subtac/subtac_command.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_command.ml')
| -rw-r--r-- | contrib/subtac/subtac_command.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml index cab8829dbd..1220c13f4d 100644 --- a/contrib/subtac/subtac_command.ml +++ b/contrib/subtac/subtac_command.ml @@ -56,7 +56,6 @@ let interp_gen kind isevars env ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[])) c = let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars (Evd.evars_of !isevars) env c in - let c' = Subtac_utils.rewrite_cases env c' in (* (try trace (str "Pretyping " ++ my_print_constr_expr c) with _ -> ()); *) let c' = SPretyping.pretype_gen isevars env ([],[]) kind c' in evar_nf isevars c' |