aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf
Commit message (Expand)AuthorAge
* Moved Compat to parsing. This permits to break the dependency of theGravatar ppedrot2012-10-04
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* avoid referring to Term in constrexpr.mli and glob_term.mliGravatar letouzey2012-10-02
* Added a new tactical infoH tac, that displays the names of hypothesis created...Gravatar courtieu2012-10-01
* Correcting a comment in pattern-matching compilation.Gravatar aspiwack2012-08-24
* Added support for option Local (at module level) in Tactic Notation.Gravatar herbelin2012-08-11
* Updating headers.Gravatar herbelin2012-08-08
* Avoid Pp.std_ppcmds in Misctypes.sort_infoGravatar letouzey2012-08-07
* The tactic remember now accepts a final eqn:H option (grant wish #2489)Gravatar letouzey2012-07-09
* induction/destruct : nicer syntax for generating equations (solves #2741)Gravatar letouzey2012-07-09
* A prototype implementation of a Print Namespace command.Gravatar aspiwack2012-07-06
* Notation: a new annotation "compat 8.x" extending "only parsing"Gravatar letouzey2012-07-05
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* Internalization of pattern is done in two phases.Gravatar pboutill2012-06-14
* Extend become a mli-only file in intf/Gravatar letouzey2012-05-29
* No more Univ in grammar.cmaGravatar letouzey2012-05-29
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* Glob_term: minor formattingGravatar letouzey2012-05-29
* Pattern as a mli-only file, operations in PatternopsGravatar letouzey2012-05-29
* New files intf/constrexpr.mli and intf/notation_term.mli out of TopconstrGravatar letouzey2012-05-29
* Glob_term now mli-only, operations now in Glob_opsGravatar letouzey2012-05-29
* Tacexpr as a mli-only, the few functions there are now in TacopsGravatar letouzey2012-05-29
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
* Evar_kinds.mli containing former Evd.hole_kind, avoid deps on EvdGravatar letouzey2012-05-29
* Decl_kinds becomes a pure mli file, remaining ops in new file kindops.mlGravatar letouzey2012-05-29
* Vernacexpr is now a mli-only file, locality stuff now in locality.mlGravatar letouzey2012-05-29