aboutsummaryrefslogtreecommitdiff
path: root/plugins/firstorder
AgeCommit message (Expand)Author
2014-05-12Now parsing rules of ML-declared tactics are only made available after thePierre-Marie Pédrot
2014-05-06Correct rebase on STM code. Thanks to E. Tassi for help on dealing withMatthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-03-01Fixing pervasive comparisonsPierre-Marie Pédrot
2014-02-27Proofview.Notations: Now that (>>=) is free, use it for tclBIND.Arnaud Spiwack
2013-12-02Writing [cut] tactic using the new monad.Pierre-Marie Pédrot
2013-11-27Adding generic solvers to term holes. For now, no resolution mechanism norPierre-Marie Pédrot
2013-11-08Porting Tactics.assumption to the new engine.ppedrot
2013-11-02Makes the new Proofview.tactic the basic type of Ltac.aspiwack
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
2013-10-24Turn many List.assoc into List.assoc_fletouzey
2013-09-27Removing a bunch of generic equalities.ppedrot
2013-08-08Vernac classification streamlined (handles VERNAC EXTEND)gareuselesinge
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-04-15More functional implementation of locality_flag and program_modegareuselesinge
2013-03-23Minor code cleaning in CArray / CList.ppedrot
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 9)letouzey
2013-03-12Term.dest* functions now raise specific DestKO exn instead of Invalid_argumentletouzey
2013-02-18use List.rev_map whenever possibleletouzey
2013-01-28Uniformization of the "anomaly" command.ppedrot
2012-12-14Modulification of identifierppedrot
2012-12-14Moved Intset and Intmap to Int namespace.ppedrot
2012-11-13More monomorphizationsppedrot
2012-10-16Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterpletouzey
2012-10-04Moved Compat to parsing. This permits to break the dependency of theppedrot
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-09-14As r15801: putting everything from Util.array_* to CArray.*.ppedrot
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-09-14The new ocaml compiler (4.00) has a lot of very cool warnings,regisgia
2012-08-08Updating headers.herbelin
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-06-01Getting rid of Pp.msgnl and Pp.message.ppedrot
2012-05-29remove many excessive open Util & Errors in mli'sletouzey
2012-05-29place all files specific to camlp4 syntax extensions in grammar/letouzey
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
2012-05-29Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evdletouzey
2012-05-29Vernacexpr is now a mli-only file, locality stuff now in locality.mlletouzey
2012-03-18Fixing bug #2732 (anomaly when using the tolerance for writingherbelin
2012-03-14Second step of integration of Program:msozeau
2012-03-02Noise for nothingpboutill
2011-11-24Added a DEPRECATED flag in declaration of options. For now only two options a...ppedrot
2011-11-17Merge subinstances branch by me and Tom Prince.msozeau
2011-10-18Fix bug #2227msozeau
2011-07-29Term: moved function constr_ord (a.k.a compare_constr) from Sequent to Termpuech
2011-07-29Sequent: generic equality on global_reference replaced by RefOrdered.comparepuech
2011-07-29Sequent: generic equality on kernel_name replaced by kn_ordpuech
2011-07-29Sequent: generic equality on constr replaced by destructorspuech
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 22:43:40 +0000