aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Expand)Author
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
2011-02-07Factorize code of rewrite to make way for a new implementation using themsozeau
2010-12-24Remove obsolete script univdot, update dev doc about universesglondu
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-12-23Change of nomenclature: rawconstr -> glob_constrglondu
2010-12-23Prepare change of nomenclature rawconstr -> glob_constrglondu
2010-11-08Print universes in debugging printersglondu
2010-11-07Delayed the evar normalization in error messages to the last minuteherbelin
2010-10-06Remove Explain* vernacsglondu
2010-10-04Install a printer for fconstr (ppconstr was installed twice)glondu
2010-09-30Simplify tactic(_)-bound arguments in TACTIC EXTEND rulesglondu
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-09-24dev/Makefile.oug: how to run the Oug analyser, for instance for finding dead ...letouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-07-24Updated COPYRIGHT file and header. Improved and fixed header updater.herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:27:09 +0000