aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2016-06-16Implement limited proof search and iterative deepening.Matthieu Sozeau
Fix typo in proofview
2016-06-16Typeclasses eauto based on new proof engine,Matthieu Sozeau
with full backtracking across multiple goals.
2016-06-16Typeclasses: stdlib fixes for new search algorithmMatthieu Sozeau
2016-06-16Refine 9cc95f5, unification of Let-In's, bug #3929Matthieu Sozeau
We unify types of let-ins in FO heuristic before their bodies, using cumulativity in either direction. This maintains the invariant that we are comparing terms in related types throughout unification. Also adapt test-suite file for bug #3929.
2016-06-16Small factorization in the typing flags of the kernel.Pierre-Marie Pédrot
2016-06-16Factorizing the uses of Declareops.safe_flags.Pierre-Marie Pédrot
This allows a smooth addition of various unsafe flags without wreaking havoc in the ML codebase.
2016-06-16Adding a default safe set of kernel typing flags to Declareops.Pierre-Marie Pédrot
2016-06-16Fixing a mispelling coma -> comma.Hugo Herbelin
2016-06-16Typo in comment.Hugo Herbelin
2016-06-16Fixing space in an error message.Hugo Herbelin
2016-06-16Fixing printing of Register retroknowledge.Hugo Herbelin
2016-06-16Fixing Add Parametric Relation by adding printer for binders.Hugo Herbelin
2016-06-16Adding printers for ring and field commands.Hugo Herbelin
2016-06-16Fixing printing of Function.Hugo Herbelin
2016-06-16Isolating and exporting a function for printing body of a recursive definition.Hugo Herbelin
2016-06-16Simplification in ppvernac.ml.Hugo Herbelin
2016-06-16Removing unused generalization of pr_vernac over pr_constr and pr_lconstr.Hugo Herbelin
No other changes (long only because of a change of indentation).
2016-06-16Fixing extra space in printing bullets.Hugo Herbelin
2016-06-16Fixing space in printing <+ and <: + fixing missing Inline keyword.Hugo Herbelin
Fixing : in Declare Module.
2016-06-16Fixing printing of Instance.Hugo Herbelin
2016-06-16Fixing extra space in printing abbreviations (SyntaxDefinition).Hugo Herbelin
2016-06-16Fixing printing of Polymorphic/Monomorphic.Hugo Herbelin
2016-06-16Fixing printing of Arguments.Hugo Herbelin
2016-06-16Printing notations as parsed.Hugo Herbelin
2016-06-16So as to beautify to work, do not use notations in Inductive typesHugo Herbelin
with a clause where, nor Notation, nor Fixpoints. Should be certainly improved at least for Inductive types and Fixpoints, depending on whether there is a "where" clause for instance.
2016-06-16Fixing missing substitution / printing cases of TacSelect.Pierre-Marie Pédrot
2016-06-16Fixing parsing of constr argument of ltac functions at level 8 in theHugo Herbelin
presence of entries starting with a non-terminal such as "b ^2".
2016-06-16Fixing printing of keeping hyp on the fly.Hugo Herbelin
2016-06-16Fixing printing of inversion as.Hugo Herbelin
2016-06-16Fixing extra space in printing destruct/induction as.Hugo Herbelin
2016-06-16Fixing printing of induction/destruct as.Hugo Herbelin
2016-06-16Fixing printing of pat%constr.Hugo Herbelin
2016-06-16In NMake_gen, giving to tactic do_size a grammar rule which respects the levels.Hugo Herbelin
2016-06-16Adding option "Set Reversible Pattern Implicit" to Specif.v so that anHugo Herbelin
implicit is found whether one writes (sig P) or {x|P x}.
2016-06-16Being defensive in printing implicit arguments also with manualHugo Herbelin
implicit arguments when in beautification mode.
2016-06-16A stronger invariant on the syntax of TacAssert, what allows for aHugo Herbelin
simpler re-printing of assert. Also fixing the precedence for printing "by" clause.
2016-06-16Changing rule for "*" in Operator_Properties so that, iterated, itHugo Herbelin
does not print to ** which is a keyword.
2016-06-16Protect the beautifier from change in the lexer state (typically byHugo Herbelin
calling Pcoq.parse_string, what some plugins such as coretactics, are doing, thus breaking the beautification of "Declare ML Module").
2016-06-16Not taking arguments given by name or position into account whenHugo Herbelin
computing the arguments which allows to decide which list of implicit arguments to consider when several such lists are available. For instance, "eq_refl (A:=nat)" is now interpreted as "@eq_refl nat _", the same way as if we had said: Arguments eq_refl {A} {x}.
2016-06-16Merge '/pr/206' into trunkEnrico Tassi
2016-06-16Merge PR #195: Complete is_* family of term-examining tactics.Pierre-Marie Pédrot
2016-06-16Merge 'pr/191' into trunkEnrico Tassi
2016-06-16Merge PR #211: Fix a printing typo in LtacProf.Pierre-Marie Pédrot
2016-06-16Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Pierre-Marie Pédrot
2016-06-16Merge PR #100: fresh now accepts more things than just identifiers.Pierre-Marie Pédrot
2016-06-16Fix Makefile after ssrmatching mergeEnrico Tassi
2016-06-16--print-version produces machine readable version infoEnrico Tassi
What one needs to know in 3rd party makefiles, like plugins ones, is the Coq version and the OCaml version number. This option prints the 2 values on a single line separated by spaces. The already existing --version outputs the same piece of info but in a format meant for user consumption, and hence harder to parse.
2016-06-16ideslave: do not bail out in case of XML errorEnrico Tassi
Used to be an `exit 1`, now an error message is printed on stderr. This helps people experimenting with the XML protocol.
2016-06-16Remove inappropriate comment.Maxime Dénès
2016-06-16Update CHANGESJason Gross
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 18:01:01 +0000