aboutsummaryrefslogtreecommitdiff
path: root/interp/constrarg.ml
AgeCommit message (Expand)Author
2016-01-20Update copyright headers.Maxime Dénès
2015-03-30grammar: export hypidentEnrico Tassi
2015-01-12Update headers.Maxime Dénès
2014-08-18Lazy interpretation of patterns so that expressions such as "intros H H'/H"Hugo Herbelin
2014-08-18Adding a new intro-pattern for "apply in" on the fly. Using syntaxHugo Herbelin
2014-08-05Fix [uconstr] name for argextend.Arnaud Spiwack
2014-07-29Add a type of untyped term to Ltac's value.Arnaud Spiwack
2014-04-14Closing bug #3260Julien Forest
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2013-12-19Removing the useless pattern ident genarg.Pierre-Marie Pédrot
2013-12-01Removing RefArgType generic argument.Pierre-Marie Pédrot
2013-11-30Getting rid of casted_open_constr. It was only used by thePierre-Marie Pédrot
2013-07-05Removing SortArgType.ppedrot
2013-07-02Removing the use of leveled tactics wit_tacticn. It is now handledppedrot
2013-06-27Getting rid of IntroPatternArgType.ppedrot
2013-06-21Cutting the dependency of Genarg in constr_expr, glob_constrppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 11:29:32 +0000