aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2010-04-05Tests for bug report #2244 (pattern-unification with abstraction over Meta's)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12899 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-05Partial fix to bug #2244 (ensure that pattern unification does notherbelin
abstract over Meta's by first posing the Meta's as Evar's). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12898 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-31Add documentation on the treatment of [if] and [let (x1, ... xn) := ..]msozeau
by Program. Fix some broken examples and detail the syntax of order annotations for well-founded recursion. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12897 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-30Small things about coqdoc + fixing lettuple.v test (part of bug #2289)herbelin
In coqdoc, made links to utf8 notations working and made representation of locations for notations more compact git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12896 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-30Removed hard-wiring of latin1 letters in coqdoc (see bug #2275)herbelin
(it interfered badly with utf-8: just take an utf-8 like "forall" which starts in iso-8859-1 with a "a circonflex"; nothing is lost since intentedly iso-8859-1 chars can only occur in comments and there is no ident detection in comments) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12895 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-30Small improvements around coqdoc (including fix for bug #2288)herbelin
- Local Definitions were considered Global Definitions in globalization file (bug #2288) [I made them "var" which makes them indexed like Variables, should we have an extra category just for Let's?] - the syntax of "[[" was not properly enforced in parse-comments mode - improved documentation of a few vernac file of the library - fixed a bug in Makefile.doc leading to build a bigger and bigger Library.pdf file git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12894 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-30Fixed small bugs introduced in commit 12890 (bug #2286, that comesherbelin
from a incorrect computation of logical names + bug in rendering of name-based notations, aka abbreviations or syntactic definitions). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12893 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-30Manual qualification of Mfourier.Proof in micromega to avoid ocamldep using ↵letouzey
ide/proof git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12892 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-30Improving error messages in the presence of utf-8 charactersherbelin
- A more clever strategy than the use of null spaces (in revision 12058) for collapsing multi-byte utf-8 characters into one character (toplevel.ml, 8.3 and trunk only) - Fixing discard_to_dot in the presence of iterated lexing failures - Made the lexer state aligned with the start of utf-8 chars instead of staying in the middle of multi-byte chars when a token is not recognized (lexer.ml4) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12891 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-29Several bug-fixes and improvements of coqdocherbelin
- make links to section variables working (used qualified names for disambiguation and fixed the place in intern_var where to dump them) (wish #2277) - mapping of physical to logical paths now follows coq (see bug #2274) (incidentally, it was also incorrectly seeing foobar.v as a in directory foo) - added links for notations - added new category "other" for indexing entries not starting with latin letter (e.g. notations or non-latin identifiers which was otherwise broken) - protected non-notation strings (from String.v) from utf8 symbol interpretation - incidentally quoted parseable _ in notations to avoid confusion with placeholder in the "_ + _" form of notation - improved several "Sys_error" error messages - fixed old bug about second dot of ".." being interpreted as regular dot - removed obsolete lexer in index.mll (and renamed index.mll to index.ml) - added a test-suite file for testing various features of coqdoc Things that still do not work: - when a notation is redefined several times in the same scope, only the link to the first definition works - if chars and symbols are not separated in advance, idents that immediately follow symbols are not detected (e.g. as in {True}+{True} where coqdoc sees a symbol "+{True}") - parentheses, curly brackets and semi-colon not linked in notations Things that can probably be improved: - all notations are indexed in the same category "other"; can we do better? - all non-latin identifiers (e.g. Greek letters) are also indexed in the same "other" category; can we do better? - globalization data for notations could be compacted (currently there is one line per each proper location covered by the notation) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12890 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-28Extended on-the-fly eta-expansion in coercion mechanism to sort-polymorphicherbelin
inductive types (see bug report #2250). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12889 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-28Fixing bug #2254 (inappropriate names of Zlt_gt_succ and Zlt_succ_gt)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12888 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-27Fixing bug #2279 (printing nested let-in was in exponential time)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12887 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-27Applied greenrd's patch to fix bug 2255 (injection failed toherbelin
detect indirect dependencies). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12886 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-24Fixed bug #2260 (check of resolution of all evars in the declarationherbelin
of a lemma was no longer done). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12885 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-23Updated CHANGES wrt 8.3herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12883 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-23Added automatic expansion on the left of recursive notationsherbelin
(currently only one expansion but could be virtually made user-parametrizable). Also fixed a bug in recursive notations happening with multiple-tokens separators (see Notations.v in test-suite). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12881 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-23Changing types to reflect futur separation between toplevel and ide.vgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12880 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-23infrastructure for safe marshal-based IPCvgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12879 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-23Goal generation deported into ide/coq.ml, single function to obtainvgross
all current goals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12878 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-23New functions for goals fetching.vgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12877 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-23Fix bug in backtracking.vgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12876 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-23debuggingvgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12875 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-19Removing unexpected printing of debug output (see bug report #2271).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12874 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-19Définition de GRAMMARCMA: parsing/grammar.cma n'était plus installé, ce ↵notin
qui empêchait la compilation de certaines contributions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12873 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-18kills a warning about vo in checker/safe_typingletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12872 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-18Makefile.build: (slightly) more robust sed invocation for parsing ↵letouzey
camlp4deps/use lines The build error Y. Makarov recently reported on coq-club was caused by some .ml4 having dos-style end-of-line in his source-tree, and hence \r appearing in the camlp4o commandline. We now simply discard what appears after camlp4xxx "...". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12871 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-18Myocamlbuild: slight simplification of code for .ml4letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12870 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-15Oops, don't use zeta by default.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12869 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-15Stop dropping evar constraints when building a new goal evar defs.msozeau
(Forgot the file in last commit). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12868 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-15Fix splitting evars tactics and stop dropping evar constraints whenmsozeau
building a new goal evar defs. Allow customization of the reduction function applied to subtac obligations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12867 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-12fixed minor pbs with test casesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12865 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-12fixed confusion between number of cstr arguments and number of pattern ↵barras
variables (which include let-ins in cstr type) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12864 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-11introduced lazy computation of size info in the guard conditionbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12862 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-11Update manual on search commandspuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12861 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-11Minimal test suite for search commandspuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12860 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-11fix [Search] when the result has no hypothesis & constant comparisonpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12859 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-11No delta-reduction in libtypes anymorepuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12858 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-11Filter out "_subproof" objects from search resultspuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12857 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-10NMake: remove useless tactics abstract_pair, nicer commentsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12856 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-10NMake: Reorganization, interface for NMake_gen, explicit View, tactic ↵letouzey
destr_t, etc etc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12855 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-10NMake_gen.ml: robustness w.r.t size, remove old commented stuff about shiftlletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12854 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-08Consider OccurCheck a catchable exception.msozeau
Fix minor bug in Program wellfounded definitions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12853 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-08Application des patches envoyés par F. Besson pour micromeganotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12852 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-07Reorder resolution of type class and unification constraints.msozeau
Fix a bug in dependent elimination when treating defined variables in the context. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12851 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-07Fix lifting of constraints in generalized rewriting tactic.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12850 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-07Fix treatment of remaining unification constraints: raise a moremsozeau
informative exception if some constraints do not unify. All calls except one used to raise a less informative exception when the constraints weren't solved. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12849 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-06Fixes in rewrite and a Elimination/Case to Scheme:msozeau
- disallow dynamic generation of [case] constructs through [find_scheme] during a rewrite, as it changes the global environment and subsequent manipulations of the tactic may use an outdated environment. - use local exception names so as not to catch and hide unexpected [Not_found] exceptions. - fix lifting of constraints for dependent function types - Allow rewriting on morphisms (terms in function position) even with [rewrite] (fixes bug #2178). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12848 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-06Adding Function as keyword for coqdocthery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12847 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-05Makefile: some more cleanupletouzey
- avoid recomputing CAMLP4DEPS in the %.ml:%.ml4 rule - a macro for compiling the tools by the best ocaml compiler - use of $(if ...) rather that $ifdef - some variables of Makefile.common were not that useful (e.g. $(COQCCMX), which is $(COQCCCMO:.cmo=.cmx), used only once) - the build of coqc.* should not depend upon coqtop, only its launch (or I'm missing something) - useless $(CAMLP4EXTENDFLAGS) variable git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12846 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-18 15:12:21 +0000