aboutsummaryrefslogtreecommitdiff
path: root/interp
AgeCommit message (Expand)Author
2009-10-26New cleaning phase of the Local/Global option managementherbelin
2009-10-25Improved the treatment of Local/Global options (noneffective Local onherbelin
2009-10-21This big commit addresses two problems:soubiran
2009-10-17Fixed a notation bug when extending binder_constr with empty levelsherbelin
2009-10-09Fix bug #2162 and a name clashing bug in generalized binders.msozeau
2009-09-27Fixed error message "cannot infer the type of id" in presence ofherbelin
2009-09-17Remove useless Liboject.export_function fieldglondu
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-09-11Generalized the possibility to refer to a global name by a notationherbelin
2009-08-13Death of "survive_module" and "survive_section" (the first one washerbelin
2009-08-06- Cleaning phase of the interfaces of libnames.ml and nametab.mlherbelin
2009-08-03Added "etransitivity".herbelin
2009-07-07Jolification : tentative de supprimer les "( evd)" et associés quiaspiwack
2009-06-22Fixes for r12197, the refined evars were not returned in case fail_evarmsozeau
2009-06-18Use more consistent resolution parameters in Program and regular typingmsozeau
2009-06-07- Added two new introduction patterns with the following temptative syntaxes:herbelin
2009-05-09- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalenceherbelin
2009-04-30Fix a small notation/scope bug:vsiles
2009-04-27- Cleaning (unification of ML names, removal of obsolete code,herbelin
2009-04-08Some dead code removal + cleanupsletouzey
2009-03-28Rewrite of Program Fixpoint to overcome the previous limitations: msozeau
2009-03-20Many changes in the Makefile infrastructure + a beginning of ocamlbuildletouzey
2009-02-19On remplace evar_map par evar_defs (seul evar_defs est désormais exporté aspiwack
2009-02-06pushed evar reduction in kernelbarras
2009-02-06Fixing #2044 (bad printing of primitive notation at the head ofherbelin
2009-01-20Fixing a bug in 11804 (support for _ in ident entry of notations). herbelin
2009-01-19- Structuring Numbers and fixing Setoid in stdlib's doc.herbelin
2009-01-17DISCLAIMERpuech
2009-01-01Switched to "standardized" names for the properties of eq andherbelin
2008-12-29- Added support for subterm matching in SearchAbout.herbelin
2008-12-14Generalized binding syntax overhaul: only two new binders: `() and `{},msozeau
2008-11-09More factorization of inductive/record and typeclasses: move classmsozeau
2008-11-05Move Record desugaring to constrintern and add ability to use notationsmsozeau
2008-10-26Correct enormous bug in interpretation of generalized binders: it simplymsozeau
2008-10-23Open notation for declaring record instances.msozeau
2008-10-23Generalized implementation of generalization.msozeau
2008-10-22Fix bugs #1975 and #1976.msozeau
2008-10-22A much better implementation of implicit generalization:msozeau
2008-10-22Affichage des notations récursives:herbelin
2008-10-19- Export de pattern_ident vers les ARGUMENT EXTEND and co.herbelin
2008-10-14Dumpglob.dump_modref : fix an assert failureletouzey
2008-10-11Backporting 11445 from 8.2 to trunk (negative conditions inherbelin
2008-10-08Améliorations de l'affichage des coercions suggérées par Georges :herbelin
2008-09-15Fix bug #1943 and restrict the inference optimisation of Program tomsozeau
2008-09-11Add enough information to correctly globalize recursive calls in inductive andmsozeau
2008-09-07Better handling of the opacity of proof obligations, add the possibility ofmsozeau
2008-08-04Évolutions diverses et variées.herbelin
2008-07-24Suite commit 11236notin
2008-07-23Stop glob messages to be printed by default on stdout letouzey
2008-07-22Correct implementation of discharging of implicit arguments and add newmsozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-21 13:27:04 +0000