aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Expand)Author
2012-08-08Updating headers.herbelin
2012-08-05Revert "Fixing include printers"pboutill
2012-08-03Fixing include printersppedrot
2012-07-30Bigint: avoid dependency over Ppletouzey
2012-07-11Severe reorganisation of the code of tactics in Proofview.aspiwack
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-05-30Getting rid of Pp.msgppedrot
2012-05-29Some documentation of recent changes concerning interfacesletouzey
2012-05-29place all pretty-printing files in new dir printing/letouzey
2012-05-29Extend become a mli-only file in intf/letouzey
2012-05-29Split Egrammar into Egramml and Egramcoqletouzey
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-05-29Strongly reduce the dependencies of grammar.cma, modulo two hacksletouzey
2012-05-29Pattern as a mli-only file, operations in Patternopsletouzey
2012-05-29Glob_term now mli-only, operations now in Glob_opsletouzey
2012-05-29Tacexpr as a mli-only, the few functions there are now in Tacopsletouzey
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
2012-05-29Vernacexpr is now a mli-only file, locality stuff now in locality.mlletouzey
2012-04-27Coqide MacOS integration refreshpboutill
2012-04-12lib directory is cut in 2 cma.pboutill
2012-04-06Removing Dhyp from debugger.herbelin
2012-03-14Everything compiles again.msozeau
2012-03-02Noise for nothingpboutill
2012-02-01Debugger vs tracer: Two different behaviors wrt printing: The debuggerherbelin
2012-01-20Added new command "Set Parsing Explicit" for deactivating parsing (andherbelin
2011-12-18Suspending declaration of undefined debug printers.herbelin
2011-11-21Renamig support added to "Arguments"gareuselesinge
2011-11-17Merge subinstances branch by me and Tom Prince.msozeau
2011-10-25First attempt at making Print Assumption compatible with opaque modules (fix ...letouzey
2011-10-17Revert "New evar_map printer ppevmfull which can typically be installed for"herbelin
2011-10-17New evar_map printer ppevmfull which can typically be installed forherbelin
2011-10-15dev/base_include: display a nice message at the end of the loadletouzey
2011-10-15debugging.txt: no more typing of #use "include" if using .ocamlinitletouzey
2011-10-11Moved to a more standard order of arguments (i.e. env followed by evar_map)herbelin
2011-10-01Moving never-used comments from Zhints.v to dev/doc so as not toherbelin
2011-09-25Polishing commits r14492, r14448 and r14407 (tactics propagateherbelin
2011-08-04Fix unification: detect invalid evar instantiations due to scoping earlier.msozeau
2011-07-29Add printer dependency to Hashtbl_alt (used in Term)puech
2011-07-18Fixed a "feature" of "inversion" and "dependent rewrite" revealed byherbelin
2011-07-16Finally, pr_goal seems to work for printing v8.2 style goal in debugger.herbelin
2011-06-21Cleaning debugging printer relative to new proof engine. Inherbelin
2011-06-13A few comments and a dev file to summarize issues with unificationherbelin
2011-05-13A new mechanism to handle errors.aspiwack
2011-05-03As many notation for for vectors as for List.pboutill
2011-04-26dev/base_include: no more mod_self_idletouzey
2011-04-13- Remove create_evar_defsmsozeau
2011-04-06Fix dev/base_include after change of constant_bodyletouzey
2011-03-16Adapt printers.mllib after my last commitletouzey
2011-02-11Annotations at functor applications:letouzey
2011-02-11Update changelogsglondu
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 18:29:24 +0000