aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Collapse)AuthorAge
* Made option "Automatic Introduction" active by default before too manyGravatar herbelin2010-06-08
| | | | | | | people use the undocumented "Lemma foo x : t" feature in a way incompatible with this activation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13090 85f007b7-540e-0410-9357-904b9bb8a0f7
* Typo in ExtrOcamlString: list char instead of char listGravatar letouzey2010-06-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13089 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix treatment of {struct x} annotations in presence of generalizedGravatar msozeau2010-06-08
| | | | | | | binders. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13086 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added support for Ltac-matching terms with variables bound in the patternGravatar herbelin2010-06-06
| | | | | | | | | | | | | | | | | | - Instances found by matching.ml now collect the set of bound variables they possibly depend on in the pattern (see type Pattern.extended_patvar_map); the variables names are canonically ordered so that non-linear matching takes actual names into account. - Removed typing of matching constr instances in advance (in tacinterp.ml) and did it only at use time (in pretyping.ml). Drawback is that we may have to re-type several times the same term but it is necessary for considering terms with locally bound variables of which we do not keep the type (and if even we had kept the type, we would have to adjust the indices to the actual context the term occurs). - A bit of documentation of pattern.mli, matching.mli and pretyping.mli. - Incidentally add env while printing idtac messages. It seems more correct and I hope I did not break some intended existing behavior. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13080 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: attempt to provide nice extraction of chars and strings for OcamlGravatar letouzey2010-06-04
| | | | | | | | | | | | | | When Requiring ExtrOcamlString : * ascii is mapped to Ocaml's char, the ugly translation of constructor and pattern-match should hopefully be seen very rarely (never ?). We add a hack in ocaml.ml for recognizing constant chars. * string is mapped to (list char). Extracting to Ocaml's string could be done, but would be really nasty (lots of non-trivial Extract Constant to add). For now, (list char) seems a good compromise. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13078 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: finish ExtrOcamlNatInt, add similar translation nat==>big_intGravatar letouzey2010-06-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13074 85f007b7-540e-0410-9357-904b9bb8a0f7
* plugins/xml: kill two warningsGravatar letouzey2010-06-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13065 85f007b7-540e-0410-9357-904b9bb8a0f7
* Misc fixes related to new nsatz (and ocamlbuild)Gravatar letouzey2010-06-03
| | | | | | | | | - Kill a warning in ideal.ml corresponding to really brain-dead code. - Restore extraction/vo.otarget in pluginsvo.itarget - In fact, plugins/_tags can be merged into _tags with nice ** patterns - Update .gitignore git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13062 85f007b7-540e-0410-9357-904b9bb8a0f7
* nsatz ajouteGravatar pottier2010-06-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13058 85f007b7-540e-0410-9357-904b9bb8a0f7
* plugin groebner updated and renamed as nsatz; first version of the doc of ↵Gravatar pottier2010-06-03
| | | | | | nsatz in the refman git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13056 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix typosGravatar glondu2010-06-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13053 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: start of a support libraryGravatar letouzey2010-06-02
| | | | | | | | | | | | - ExtrOcamlBasic: mapping of basic types to ocaml's ones - ExtrOcamlIntConv: conversion between int and coq's numerical types - ExtrOcamlBigIntConv: same with big_int (no overflow) - ExtrOcamlNatInt: realizes nat by int (unsafe) more to come: Haskell, handling of stings, more stuff in ExtrOcamlNatInt, etc etc... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13050 85f007b7-540e-0410-9357-904b9bb8a0f7
* A little bit of cleanup, and some annotations.Gravatar fkirchne2010-05-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13036 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modify the test for csdp and associated message.Gravatar fkirchne2010-05-28
| | | | | | Use the refactored system.ml function. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13034 85f007b7-540e-0410-9357-904b9bb8a0f7
* ...Gravatar fkirchne2010-05-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13032 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extract Inductive is now possible toward non-inductive types (e.g. nat => int)Gravatar letouzey2010-05-21
| | | | | | | | | | | For instance: Extract Inductive nat => int [ "0" "succ" ] "(fun fO fS n => if n=0 then fO () else fS (n-1))". See Extraction.v for more details and caveat. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13025 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ocamlbuild: various fixGravatar letouzey2010-05-19
| | | | | | | | | - transition to camlp4, with no compatibility for ocamlbuild+camlp5 (error message) - fix compilation of decl_mode : a forgotten include, and Decl_expr which is a pure .mli shouldn't be mentionned in the .mllib git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13020 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add (almost) compatibility with camlp4, without breaking support for camlp5Gravatar letouzey2010-05-19
| | | | | | | | | | | | | | | | | | | | | | | The choice between camlp4/5 is done during configure with flags -usecamlp5 (default for the moment) vs. -usecamlp4. Currently, to have a full camlp4 compatibility, you need to change all "EXTEND" and "GEXTEND Gram" into "EXTEND Gram", and change "EOI" into "`EOI" in grammar entries. I've a sed script that does that (actually the converse), but I prefer to re-think it and check a few things before branching this sed into the build mechanism. lib/compat.ml4 is heavily used to hide incompatibilities between camlp4/5 and try to propose a common interface (cf LexerSig / GrammarSig). A few incompatible quotations have been turned into underlying code manually, in order to make the IFDEF CAMLP5 THEN ... ELSE ... END parsable by both camlp4 and 5. See in particular the fate of <:str_item< declare ... end >> Stdpp isn't used anymore, but rather Ploc (hidden behind local module Loc). This forces to use camlp5 > 5.01. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13019 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove refutpat.ml4, ideal.ml4 is again a normal .ml, let* coded in a naive wayGravatar letouzey2010-05-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13017 85f007b7-540e-0410-9357-904b9bb8a0f7
* static (and shared) camlp4use instead of per-file declarationGravatar letouzey2010-05-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13016 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove compile-command pragmas for emacsGravatar letouzey2010-05-19
| | | | | | | | | | | | | | | | | | | These declarations (e.g. make -C .. bin/coqtop.byte) are quite annoying when debugging stuff over the whole archive: all of a sudden, M-x recompile isn't doing what you intended just because you've visited some specific files. Instead: - Feel free to rather add intermediate targets in the Makefile if they aren't there yet. - For avoiding typing the -C with many .. after, you can have a look at my recursively-descending make: http://www.pps.jussieu.fr/~letouzey/download/make.sh which is to be renamed make and placed in a bin dir with more priority than /usr/bin. Beware! I've already add a few bad surprises with this hack, but it's really convenient nonetheless. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13014 85f007b7-540e-0410-9357-904b9bb8a0f7
* Applicative commutative cuts in Fixpoint guard conditionGravatar pboutill2010-05-18
| | | | | | | | | | | | | | | | | | | | | In "(match ... with |... -> fun x -> t end) u", "x" has now the subterm property of "u" in the analysis of "t". Commutative cuts aren't compatible with typing so we need to ensure that term of "x"'s type and term of "u"'s have the same subterm_spec. Consequently,declaration.MRec argument has changed to the inductive name instead of only the number of the inductive in the mutual_inductive family. In subterm_specif and check_rec_call, arguments are stored in a stack. At each lambda, one element is popped to add in renv a smarter subterm_spec for the variable. subterm_spec of constructor's argument was added this way, the job is now done more often. Some eta contracted match branches are now accepted but enforcing eta-expansion of branches might be anyway a recommended invariant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13012 85f007b7-540e-0410-9357-904b9bb8a0f7
* better detection of nested recursion in FunctionGravatar jforest2010-05-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13001 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction of a bug pointed by P. Casteran.Gravatar jforest2010-05-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12998 85f007b7-540e-0410-9357-904b9bb8a0f7
* Trying to find a problem pointed by P. CasteranGravatar jforest2010-05-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12997 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction of bug 2290 (removing stupid message)Gravatar jforest2010-05-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12990 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction of bug 2290Gravatar jforest2010-05-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12989 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: fix type_expunge_from_sign broken in last commitGravatar letouzey2010-05-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12983 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: an experimental command to get rid of some cst/constructor argumentsGravatar letouzey2010-04-30
| | | | | | | | | | | | The command : Extraction Implicit foo [1 3]. will tell the extraction to consider fst and third arg of foo as implicit, and remove them, unless a final occur-check after extraction shows they are still there. Here, foo can be a inductive constructor or a global constant. This allow typicaly to extract vectors into usual list :-) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12982 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
| | | | | | | | | | | - Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
* Misc small fixes : warning, dep cycles, ocamlbuild...Gravatar letouzey2010-04-26
| | | | | | | | | | | | - git ignore g_decl_mode.ml - exhaustive match for pp_vernac (BeginSubproof, ...) - for ocamlbuild, remove a spurious cycle in recordops.mli (unnecessary open of Classops), and fixes of *.itargets and _tags The compilation via ocamlbuild still need some work, since plugin firstorder now depends on the new plugin decl_mode git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12964 85f007b7-540e-0410-9357-904b9bb8a0f7
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a fairly large commit (around 140 files and 7000 lines of code impacted), it will cause some troubles for sure (I've listed the know regressions below, there is bound to be more). At this state of developpement it brings few features to the user, as the old tactics were ported with no change. Changes are on the side of the developer mostly. Here comes a list of the major changes. I will stay brief, but the code is hopefully well documented so that it is reasonably easy to infer the details from it. Feature developer-side: * Primitives for a "real" refine tactic (generating a goal for each evar). * Abstract type of tactics, goals and proofs * Tactics can act on several goals (formally all the focused goals). An interesting consequence of this is that the tactical (. ; [ . | ... ]) can be separated in two tacticals (. ; .) and ( [ . | ... ] ) (although there is a conflict for this particular syntax). We can also imagine a tactic to reorder the goals. * Possibility for a tactic to pass a value to following tactics (a typical example is an intro function which tells the following tactics which name it introduced). * backtracking primitives for tactics (it is now possible to implement a tactical '+' with (a+b);c equivalent to (a;c+b;c) (itself equivalent to (a;c||b;c)). This is a valuable tool to implement tactics like "auto" without nowing of the implementation of tactics. * A notion of proof modes, which allows to dynamically change the parser for tactics. It is controlled at user level with the keywords Set Default Proof Mode (this is the proof mode which is loaded at the start of each proof) and Proof Mode (switches the proof mode of the current proof) to control them. * A new primitive Evd.fold_undefined which operates like an Evd.fold, except it only goes through the evars whose body is Evar_empty. This is a common operation throughout the code, some of the fold-and-test-if-empty occurences have been replaced by fold_undefined. For now, it is only implemented as a fold-and-test, but we expect to have some optimisations coming some day, as there can be a lot of evars in an evar_map with this new implementation (I've observed a couple of thousands), whereas there are rarely more than a dozen undefined ones. Folding being a linear operation, this might result in a significant speed-up. * The declarative mode has been moved into the plugins. This is made possible by the proof mode feature. I tried to document it so that it can serve as a tutorial for a tactic mode plugin. Features user-side: * Unfocus does not go back to the root of the proof if several Focus-s have been performed. It only goes back to the point where it was last focused. * experimental (non-documented) support of keywords BeginSubproof/EndSubproof: BeginSubproof focuses on first goal, one can unfocus only with EndSubproof, and only if the proof is completed for that goal. * experimental (non-documented) support for bullets ('+', '-' and '*') they act as hierarchical BeginSubproof/EndSubproof: First time one uses '+' (for instance) it focuses on first goal, when the subproof is completed, one can use '+' again which unfocuses and focuses on next first goal. Meanwhile, one cas use '*' (for instance) to focus more deeply. Known regressions: * The xml plugin had some functions related to proof trees. As the structure of proof changed significantly, they do not work anymore. * I do not know how to implement info or show script in this new engine. Actually I don't even know what they were suppose to actually mean in earlier versions either. I wager they would require some calm thinking before going back to work. * Declarative mode not entirely working (in particular proofs by induction need to be restored). * A bug in the inversion tactic (observed in some contributions) * A bug in Program (observed in some contributions) * Minor change in the 'old' type of tactics causing some contributions to fail. * Compilation time takes about 10-15% longer for unknown reasons (I suspect it might be linked to the fact that I don't perform any reduction at QED-s, and also to some linear operations on evar_map-s (see Evd.fold_undefined above)). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12961 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: cosmetics when using ocaml + Extract Inductive to symbolsGravatar letouzey2010-04-16
| | | | | | | | | | | - When using an infix constructor such as (::), whitespaces are to be given by the user, for instance Extract Inductive list => list [ "[]" "( :: )" ]. - Remove ugly whitespaces when using the ""-for-Pair trick: Extract Inductive prod => "(*)" [ "" ]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12944 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: restore (temporarily?) a very limited form of linear letin reductionGravatar letouzey2010-04-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12943 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: less eta in calls to global functions, better optimization phaseGravatar letouzey2010-04-16
| | | | | | | | | | | | - we saturate the normalize function : as long as (kill_dummy + simpl) isn't a nop, we do it again. - generalize_case allowed on all types of theories/Init/*.v instead of only bool,sumbool,sumor. NB: this optim cannot be performed on any type, it might produce untyped code. - common_branch allowed on match with one branch: in this situation it indicates whether the match can be removed or not. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12942 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: improvement of optimizations (kill_dummy, optim_fix)Gravatar letouzey2010-04-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12940 85f007b7-540e-0410-9357-904b9bb8a0f7
* Util: remove list_split_at which is a clone of list_chopGravatar letouzey2010-04-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12939 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: ad-hoc identifier type with annotations for reductionsGravatar letouzey2010-04-16
| | | | | | | | | | | | | | | | * An inductive constructor Dummy instead of a constant dummy_name * The Tmp constructor indicates that the corresponding MLlam or MLletin is extraction-specific and can be reduced if possible * When inlining a glob (for instance a recursor), we tag some lambdas as reducible. In (nat_rect Fo Fs n), the head lams of Fo and Fs are treated this way, in order for the recursive call inside nat_rect to be correctly pushed as deeper as possible. * This way, we can stop allowing by default linear beta/let reduction even under binders (can be activated back via Set Extraction Flag). * Btw, fix the strange definition of non_stricts for (x y). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12938 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: less _ in Haskell (typically for False_rect), less toplevel ↵Gravatar letouzey2010-04-16
| | | | | | eta-expansions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12936 85f007b7-540e-0410-9357-904b9bb8a0f7
* Look for csdp in $PATH at runtime, remove -csdpdir configure optionGravatar glondu2010-04-11
| | | | | | | | | The csdp path computed by the configure script wasn't used at all, but was forcing presence of csdp at configure time whereas it is not used at all in the build process. Instead, we replace the configure-time check with a runtime check for existence of csdp in $PATH. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12929 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove unused functions run_sdpaGravatar glondu2010-04-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12928 85f007b7-540e-0410-9357-904b9bb8a0f7
* Manual qualification of Mfourier.Proof in micromega to avoid ocamldep using ↵Gravatar letouzey2010-03-30
| | | | | | ide/proof git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12892 85f007b7-540e-0410-9357-904b9bb8a0f7
* Several bug-fixes and improvements of coqdocGravatar herbelin2010-03-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - 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
* Oops, don't use zeta by default.Gravatar msozeau2010-03-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12869 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix splitting evars tactics and stop dropping evar constraints whenGravatar msozeau2010-03-15
| | | | | | | | | 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
* fixed confusion between number of cstr arguments and number of pattern ↵Gravatar barras2010-03-12
| | | | | | 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
* Consider OccurCheck a catchable exception.Gravatar msozeau2010-03-08
| | | | | | | 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
* Application des patches envoyés par F. Besson pour micromegaGravatar notin2010-03-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12852 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reorder resolution of type class and unification constraints.Gravatar msozeau2010-03-07
| | | | | | | | 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
* Fix treatment of remaining unification constraints: raise a moreGravatar msozeau2010-03-07
| | | | | | | | | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 14:11:34 +0000