aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2009-09-29kills the old backtracking framework and replaces it withvgross
2009-09-26Fixed a hole in glob_tactic that allowed some Ltac code to refer toherbelin
2009-09-22Add the option to automatically introduce variables declared before themsozeau
2009-09-17Replace call to where_in_path by find_file_in_path in "Locate File"glondu
2009-09-17Replace unprotected call to where_in_path by find_file_in_pathglondu
2009-09-17Remove useless Liboject.export_function fieldglondu
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-09-15Fixed compilation error message which was no longer emacs-compliant sinceherbelin
2009-09-14Backtrack on the forced discharge of type class variables introducedmsozeau
2009-09-14- Addition of "Reserved Infix" continued.herbelin
2009-09-11Generalized the possibility to refer to a global name by a notationherbelin
2009-09-02Postpone checking of Local/Global to allow grammar extensions to use itmsozeau
2009-09-02Stop unnecessary use of lazy values for constraints, simplifyingmsozeau
2009-08-14Ajout de la gestion de Local et Global pour les options (au sens deaspiwack
2009-08-13Death of "survive_module" and "survive_section" (the first one washerbelin
2009-08-11Add support for "Infix ... := constr" instead of just "Infix ... := ref".herbelin
2009-08-06- Cleaning phase of the interfaces of libnames.ml and nametab.mlherbelin
2009-08-04- Add more precise error localisation when one of the application failsherbelin
2009-08-03Added "etransitivity".herbelin
2009-08-02Improved parameterization of Coq:herbelin
2009-07-08Use user-given implicits from the arity in inductive definitions.msozeau
2009-07-07Jolification : tentative de supprimer les "( evd)" et associés quiaspiwack
2009-07-01Support for binding Coq root read-only in -R optionherbelin
2009-06-18Use more consistent resolution parameters in Program and regular typingmsozeau
2009-06-18Fix "unsatisfiable constraints" error messages to include all themsozeau
2009-06-13Correct typo: -noglob takes no argument.msozeau
2009-06-11Use a lazy value for the message in FailError, so that it won't bemsozeau
2009-05-27Fix implicit args code so that declarations are added for allmsozeau
2009-05-27Stop using a "Manual Implicit Arguments" flag and support them as soonmsozeau
2009-05-16Minor fixes in typeclasses:msozeau
2009-05-13 Fix to my last notation patch: now fixpoint are correctly handled vsiles
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- Fixed a little bug in previous commit (bad failure in case of unknown entry).herbelin
2009-04-27- Cleaning (unification of ML names, removal of obsolete code,herbelin
2009-04-25- Fixing #2090 (occur check missing when trying to solve evar-evar equation).herbelin
2009-04-24Backporting 12080 (fixing bug #2091 on bad rollback in the "where"herbelin
2009-04-16Fix bug #2089: correctly dealing with parameters and real arguments inmsozeau
2009-04-08Some dead code removal + cleanupsletouzey
2009-04-08- Fixing bug #2084 (unification not checking sort constraints), hopingherbelin
2009-04-08- Backport of 12053 (fixing parsing segfault bug #2087) and 12058 (fixingherbelin
2009-03-28Rewrite of Program Fixpoint to overcome the previous limitations: msozeau
2009-03-27Remove unused mli filesletouzey
2009-03-22Backport from v8.2 branch of 11986 (interpretation of quantifiedherbelin
2009-03-20Many changes in the Makefile infrastructure + a beginning of ocamlbuildletouzey
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey
2009-03-17- configure: affiche si le natdynlink est positionnebarras
2009-03-16Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"herbelin
2009-03-14Better mechanism for loading initial pluginsletouzey
2009-03-09Optionally list opaque constants in addition to axions/variables inmsozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 19:46:24 +0000