diff options
Diffstat (limited to 'plugins/ltac/extratactics.ml4')
| -rw-r--r-- | plugins/ltac/extratactics.ml4 | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 3e3965b94..10be8a842 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - open Pp open Genarg open Stdarg @@ -73,7 +71,7 @@ END let induction_arg_of_quantified_hyp = function | AnonHyp n -> None,ElimOnAnonHyp n - | NamedHyp id -> None,ElimOnIdent (Loc.tag id) + | NamedHyp id -> None,ElimOnIdent (CAst.make id) (* Versions *_main must come first!! so that "1" is interpreted as a ElimOnAnonHyp and not as a "constr", and "id" is interpreted as a |