aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)Gravatar Pierre Letouzey2014-03-02
| | | | | | | There are currently two other clashs : Lexer and Errors, but for the moment these ones haven't impacted my experiments with extraction and compiler-libs, while this Matching issue had. And anyway the new name is more descriptive, in the spirit of the recent TacticMatching.
* Set officially the minimal OCaml requirement to 3.12.1Gravatar Pierre Letouzey2014-03-02
| | | | | | | | | | | | | | | Anyway, a few syntactic features of 3.12 were already used here and there (e.g. local opening via Foo.(...), or the record shortcut { field; ... }). Hence compiling with 3.11 wasn't working anymore. Already take advantage of the following 3.12.1 features : - "module type of ..." in CArray, CList, CString ... - "ocamldep -ml-synonym" : no need anymore to hack the ocamldep output via our coqdep to localize the .ml4 modules :-) The -ml-synonym option (+ various bugfixes) is the reason for asking 3.12.1 directly and not just 3.12.0. After all, if debian stable is providing 3.12.1, then everybody has it ;-)
* Makefile: the initial build of grammar.cma is now directory-drivenGravatar Pierre Letouzey2014-03-02
| | | | | | | | | | | | | In last commit, we used grep to decide whether a .ml4 could be compiled during the initial phase of not. Instead, we now rely on a simpler directory dichotomy: - config lib kernel library pretyping interp parsing grammar are considered initial (and shouldn't contain grammar-dependent .ml4), see $(GRAMSRCDIRS) in Makefile.common - the grammar-dependent .ml4 could be in any other directories Currently, they are in: tactics toplevel plugins/*
* Migrate back g_obligations in toplevelGravatar Pierre Letouzey2014-03-02
| | | | | | | | | | | | | | | | This almost reverts commit 845d6f (r15248). It isn't ideal to put syntactic stuff in the toplevel directory. Maybe this kind of files should have someday their own directory along with g_rewrite.ml4 and some other (maybe a extraparsing dir?). Meanwhile, this commit leads to a cleaner situation concerning *.ml4: - everything needed to build grammar.cma (and q_constr.cmo) is in: lib/ kernel/ library/ pretyping/ interp/ proofs/ parsing/ grammar/ - all *.ml4 using grammar.cma (or q_constr.cmo) are in: tactics/ toplevel/ plugins/*/
* Grammar.cma with less deps (Glob_ops and Nameops) after moving minor codeGravatar Pierre Letouzey2014-03-02
| | | | | NB: new file miscprint.ml deserves to be part of printing.cma, but should be part of proofs.cma for the moment, due to use in logic.ml
* Removing generic equality in Syntax plugin.Gravatar Pierre-Marie Pédrot2014-03-02
|
* Adding an equality function over glob_constrGravatar Pierre-Marie Pédrot2014-03-02
|
* Fixing generic Hashtbl.hash in Constr.Gravatar Pierre-Marie Pédrot2014-03-02
|
* Fix syntax highlighting of "Implicit Arguments" for gtksourceview.Gravatar Guillaume Melquiond2014-03-02
|
* Fixing pervasive comparisonsGravatar Pierre-Marie Pédrot2014-03-01
|
* Better behaviour for sets of reserved names.Gravatar Pierre-Marie Pédrot2014-03-01
|
* Never suppress the typing constraint of bound variables whose name wasGravatar Pierre-Marie Pédrot2014-03-01
| | | | reserved with Implicit Type.
* Fixing bad comparison in Detyping.Gravatar Pierre-Marie Pédrot2014-03-01
|
* Useless check when loading notations through import.Gravatar Pierre-Marie Pédrot2014-03-01
|
* Hunting pervasive equality in native compiler. It seems they were used forGravatar Pierre-Marie Pédrot2014-03-01
| | | | | optimization purposes. I replaced their use with the under-approximation of pointer equality.
* Removing a fishy use of pervasive equality in Ltac backtrace printing.Gravatar Pierre-Marie Pédrot2014-03-01
|
* Removing Pervasives.compare in Termdn.Gravatar Pierre-Marie Pédrot2014-02-28
|
* Removing a Pervasives.compare in Term_dnet.Gravatar Pierre-Marie Pédrot2014-02-28
|
* Pos.compare_cont takes the comparison as first argumentGravatar Pierre Boutillier2014-02-28
| | | | Helps cbn tactic refolding
* Fix bug 3245: 'simpl nomatch' argument annotation makes cbn go into an ↵Gravatar Pierre Boutillier2014-02-28
| | | | infinite loop.
* test-suite: opaque term -> opaque proofGravatar Pierre Boutillier2014-02-28
|
* test-suite: New names for vars but the expected invariant is preservedGravatar Pierre Boutillier2014-02-28
|
* Fix output test-suite 'simpl tactic' -> 'reduction tactics'Gravatar Pierre Boutillier2014-02-28
|
* Dead code elimionation in reductionopsGravatar Pierre Boutillier2014-02-28
|
* .*.aux erased by make distcleanGravatar Pierre Boutillier2014-02-28
|
* Fix compilation of coq and plugins using coq_makefile under cygwinGravatar Enrico Tassi2014-02-28
| | | | | | | | | Problems: - strip may not be "strip" but "i686-bla-strip", hence we ask ocamlc -config the value of "ranlinb" and replace ranlib by strip obtaining "i686-bla-strip" from "i686-bla-ranlib" - coq_makefile was not quoting the plugins/ paths - coq_makefile was quoting twice camlpX (the shell of cygwin was confused)
* Fixing a Pervasive.compare.Gravatar Pierre-Marie Pédrot2014-02-28
|
* Makefile: re-introduce 2 phases to avoid make strange -include'sGravatar Pierre Letouzey2014-02-27
| | | | | | | | | | | | | | | | | | | | | | | | | Yet another revision of the build system. We avoid relying on the awkward include-which-fails-but-works-finally-after-a-retry feature of gnu make. This was working, but was quite hard to understand. Instead, we reuse the idea of two explicit phases (as in 2007 and its stage{1,2,3}), but in a lighter way. The main Makefile calls Makefile.build twice : - first for building grammar.cma (and q_constr.cmo), with a restricted set of .ml4 to consider (see variables BUILDGRAMMAR and ML4BASEFILES). - then on the true target(s) asked by the user (using the special variable MAKECMDGOALS). In pratice, this should change very little to the concrete developper's life, let me know otherwise. A few more messages of make due to the explicit first sub-call, but no more strange "not ready yet" messages... Btw: we should handle correctly now the parallel compilation of multiple targets (e.g. make -jX foo bar). As reported by Pierre B, this was triggering earlier two separate sub-calls to Makefile.build, one for foo, the other for bar, with possibly nasty interactions in case of parallelism. In addition, some cleanup of Makefile.build, removal of useless :: rules, etc etc.
* amending last commitGravatar Enrico Tassi2014-02-27
|
* better warningGravatar Enrico Tassi2014-02-27
|
* Tacinterp: more refactoring.Gravatar Arnaud Spiwack2014-02-27
| | | Introducing List.fold_right and List.fold_left in Monad.
* Tacinterp: refactoring using Monad.Gravatar Arnaud Spiwack2014-02-27
| | | Adds a combinator List.map_right which chains effects from right to left.
* Code refactoring thanks to the new Monad module.Gravatar Arnaud Spiwack2014-02-27
|
* Remove unsafe code (Obj.magic) in Tacinterp.Gravatar Arnaud Spiwack2014-02-27
| | | This commit also introduces a module Monad to generate monadic combinators (currently, only List.map).
* Proofview.Notations: Now that (>>=) is free, use it for tclBIND.Gravatar Arnaud Spiwack2014-02-27
| | | | Impacts MapleMode.
* Get rid of the enterl/glist API for Proofview.Goal.Gravatar Arnaud Spiwack2014-02-27
| | | The prefered style is to use continuation passing style when necessary, or simply passing the goal explicitely in the case of interpretation functions which do not evolve the current goal.
* Tacinterp: yet another superfluous enterl.Gravatar Arnaud Spiwack2014-02-27
|
* Tacinterp: spurious enterl.Gravatar Arnaud Spiwack2014-02-27
| | | This changes the tacinterp API, but only affects (one line of) the MapleMode contrib.
* Dead code: eval_ltac_constr.Gravatar Arnaud Spiwack2014-02-27
|
* STM: better debug messagesGravatar Enrico Tassi2014-02-26
|
* STM: do not print goals on UndoGravatar Enrico Tassi2014-02-26
|
* CoqIDE: print message of "Fail" commandGravatar Enrico Tassi2014-02-26
|
* refman: document vi2voGravatar Enrico Tassi2014-02-26
|
* STM: better messages when checking/finishing tasksGravatar Enrico Tassi2014-02-26
|
* Library: when compiling multiple files, reset the opaque tablesGravatar Enrico Tassi2014-02-26
| | | | | That was a bug. coqc a b was generating (for b) an opaque table containing also the proofs of a.
* STM: when batch compiling a vo, assert we behave conservativelyGravatar Enrico Tassi2014-02-26
| | | | | This meas that the list of future_constraints in safe_env is empty, meaning that nothing was delayed.
* coq_makefile: new target vi2voGravatar Enrico Tassi2014-02-26
|
* vi2vo: new flag -schedule-vi2voGravatar Enrico Tassi2014-02-26
|
* Lazyconstr -> OpaqueproofGravatar Enrico Tassi2014-02-26
| | | | | Make this module deal only with opaque proofs. Make discharging/substitution invariant more explicit via a third constructor.
* STM: backup/restore remote countersGravatar Enrico Tassi2014-02-26
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-15 07:16:03 +0000