aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Error messages of Searchxxx are coherent with goal selector.Gravatar Pierre Courtieu2014-12-16
| | | | | | If a goal is given and wrong, exception is raised. If no goal is given, then goal 1 is tried but no failure if goal 1 does not exist, just fall back to gloab env.
* Fix for #3154: use CUnix.sys_command to call native compiler.Gravatar Maxime Dénès2014-12-16
| | | | | Patch by CJ on bugzilla. CUnix.sys_command doesn't rely on a shell, so extra care with cmd.exe vs sh is no longer required.
* Changed bullet informations to warning for better display in PG.Gravatar Pierre Courtieu2014-12-15
| | | | | Since it displays together with the goal, it is better (for pg and other interfaces probably) that they are in a different message.
* Adapted test file for About.Gravatar Pierre Courtieu2014-12-15
|
* Tentatively starting to use heuristics for evar-evar resolution: firstGravatar Hugo Herbelin2014-12-15
| | | | | | | | | | step, prefer QuestionMark's to other evars, to comply with the filtering made on VarInstance, GoalEvar and QuestionMark for type class resolution. Maybe evars to be resolved by type class instances should eventually be marked with a specific tag. At least, this solves the current problem with compiling cancel2.v in LemmaOverloading.
* Failing on unbound notation variable in notation level modifiersGravatar Hugo Herbelin2014-12-15
| | | | | | | + consequences of this check on the standard library (moved the no-op in Notation modifiers to what there were supposed to do; these are anyway local notations, so compatibility is safe - please AS or PL, amend if needed).
* New try on Fixing an evar_map bug revealed by commit 603b66f81 onGravatar Hugo Herbelin2014-12-15
| | | | unification flags (see also temporary revert in d083200ae5b).
* Tests for #3848 and #3854.Gravatar Hugo Herbelin2014-12-15
|
* Documenting check_record + changing a possibly undefined int into int option.Gravatar Hugo Herbelin2014-12-15
|
* About now accepts hypothesis names and goal selector.Gravatar Pierre Courtieu2014-12-15
|
* Fix treatment of universe context in typecheck inductive (was addedGravatar Matthieu Sozeau2014-12-15
| | | | twice). Thanks to Marc Lasson for spotting this.
* Tests for Searchxxx commands added and modified.Gravatar Pierre Courtieu2014-12-15
|
* Fixing bug #3865.Gravatar Pierre-Marie Pédrot2014-12-15
|
* Util.un_op -> Option.defaultGravatar Pierre Boutillier2014-12-14
|
* Fix merging of name maps in union of universe contexts.Gravatar Matthieu Sozeau2014-12-14
|
* Fixing bug #3858 and #3817 in one stroke.Gravatar Pierre-Marie Pédrot2014-12-14
|
* Revert "Fixing bug #3817."Gravatar Pierre-Marie Pédrot2014-12-14
| | | | This reverts commit ad2a0308b1592c7235714a2cca926f3b55accbb2.
* Add Ltac syntax for the [tclIFCATCH] primitive.Gravatar Arnaud Spiwack2014-12-12
| | | | [tryif t then t2 else t3] behaves like [t;t2] if [t] has at least one success, or [t3] otherwise. It generalises [t||t3] as failures from [t2] will not be caught.
* Make sure the goals on the shelve are identified as goal and unresolvable ↵Gravatar Arnaud Spiwack2014-12-12
| | | | | | | for typeclasses. This was not the case for goals created at the end of the tactic by salvaging the [future_goals] from the evar map. It would cause typeclass resolution to try and solve these goals (if they have a class type) at each subsequent tactic. Fixes #3841.
* Searchxxx now interpret patterns in goal environment if any.Gravatar Pierre Courtieu2014-12-12
| | | | | | | | | | | This makes such things work: x:nat h: x = 3 ================ True Search x.
* #4843 part 2 : The .cmxs files for plug-ins must have execute permissionGravatar Pierre Boutillier2014-12-12
|
* Fix #3163 and #3843 part 1 : Cygwin DLLs have extension ".so", not ".dll"Gravatar Pierre Boutillier2014-12-12
|
* Fix #3800 : cmxs need execution priviledges under windowsGravatar Pierre Boutillier2014-12-12
|
* An option SimplIsCbnGravatar Pierre Boutillier2014-12-12
|
* Extend the syntax of simpl with a delta flag.Gravatar Arnaud Spiwack2014-12-12
| | | | You can write 'simpl -[plus minus] div2'. Simpl does not use it for now.
* Searchxxx now search also the hypothesis and support goal selector.Gravatar Pierre Courtieu2014-12-12
| | | | Documentation also updated.
* Two fixes in unification (bugs #3782 and #3709)Gravatar Matthieu Sozeau2014-12-12
| | | | | | | | - In evarconv, check_conv_record properly computes the parameters of primitive record projections for later unification, adding env and sigma as arguments. - In unification, backtrack on pattern-unification and not only application unification if eta for a record failed.
* In discrimination nets, do not index lambdas if they're part of a betaGravatar Matthieu Sozeau2014-12-12
| | | | redex.
* handling Functional Scheme for required but not imported modulesGravatar Julien Forest2014-12-11
|
* List.v: sequel to Sebastien's commit (some cosmetics + a few shorter proofs)Gravatar Pierre Letouzey2014-12-11
|
* First series of results on lists.Gravatar Sébastien Hinderer2014-12-11
|
* Commit not ready. Sorry.Gravatar Hugo Herbelin2014-12-11
| | | | | | Revert "Fixing an evar_map bug revealed by commit 603b66f81 on unification flags." This reverts commit d083200ae5b391ceffaa0329a8e3a334036c7968.
* Added a CannotSolveConstraint unification error and made experimentsGravatar Hugo Herbelin2014-12-11
| | | | in reporting the chain of causes when unification fails.
* Fine-tuning unification error (using OccurCheck in evarconv).Gravatar Hugo Herbelin2014-12-11
|
* Tentatively more informative report of failure when inferringGravatar Hugo Herbelin2014-12-11
| | | | pattern-matching predicate.
* Fixing an evar_map bug revealed by commit 603b66f81 on unification flags.Gravatar Hugo Herbelin2014-12-11
| | | | This fixes current failure of RelationAlgebra.
* Test suite: keep message in sync with actual file deletions.Gravatar Xavier Clerc2014-12-11
|
* Ignore *.vi files, just like *.vo files.Gravatar Xavier Clerc2014-12-11
|
* New reproduction cases for the test suite.Gravatar Xavier Clerc2014-12-11
|
* Fix dummy argument use in guess_elim: there are some cases where X_indGravatar Matthieu Sozeau2014-12-10
| | | | is not defined while X_rect is, for example in HoTT/Coq.
* Revert commit that inverted the preference for FFlex/FProj problems inGravatar Matthieu Sozeau2014-12-10
| | | | kernel reduction.
* Fixing orientation of postponed subtyping problems.Gravatar Hugo Herbelin2014-12-10
| | | | | | | | | | | In the case of conversion, postponing by preserving the initial orientation. Was wrong from its initial version in Jan 2014, but was not visible because evar-evar subtyping was approximated by evar-evar conversion. Thanks to Enrico for a very short example highlighting the problem. In particular, this fixes Ergo.
* Using a more aggressive test for resolving pattern equations ?n = ?p:Gravatar Hugo Herbelin2014-12-10
| | | | | | test pattern-unification after restriction of the evars so as to succeed earlier (no observational changes however in the examples at my disposal).
* typoGravatar Enrico Tassi2014-12-10
|
* test-suite: few tests for ".v -> .vi -> .vo" compilation chainGravatar Enrico Tassi2014-12-10
|
* Setup hook to change the unification algorithm used by evarconv,Gravatar Matthieu Sozeau2014-12-09
| | | | e.g. for MTac.
* Switch the few remaining iso-latin-1 files to utf8Gravatar Pierre Letouzey2014-12-09
|
* refman: switch all source files to utf8Gravatar Pierre Letouzey2014-12-09
| | | | | | Putting utf8 everywhere helps the maintainance of the online refman. And anyway, this is the way to go. We should also chase and migrate the few remaining iso-latin-1 files elsewhere in the sources.
* refman: fix broken urlsGravatar Pierre Letouzey2014-12-09
|
* refman: remove ?uri=referer in urls pointing to validator.w3.orgGravatar Pierre Letouzey2014-12-09
| | | | | | | | | | | Unfortunately, these ?uri=referer parameters do not work correctly now that coq.inria.fr forces the switch to https before answering any document. See: http://validator.w3.org/docs/help.html#faq-referer I currently see no workaround for that, apart from generating links like ?uri=http://the.real.url/of/my/page, which would be quite painful. For now, users interested in checking the validity of our pages will have to copy-paste the url they want to check after clicking on the validator button.
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-21 19:04:03 +0000