| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-12-17 | CoqIDE: better messages | Enrico Tassi | |
| 2014-12-17 | Revert and correctly fix "#4843 part 2 : The .cmxs files for plugins must ↵ | Pierre Boutillier | |
| have x permission" This reverts commit 607503b28fca50f4b76b2237d5ca13802b8252fa. | |||
| 2014-12-16 | #3828 is solved. | Hugo Herbelin | |
| 2014-12-16 | Moving #2447 (congruence) to fixed. | Hugo Herbelin | |
| 2014-12-16 | In CHANGES, alerting about stronger check on notation level modifiers. | Hugo Herbelin | |
| 2014-12-16 | More printers for ltac signatures. | Hugo Herbelin | |
| 2014-12-16 | Test for #3654. | Hugo Herbelin | |
| 2014-12-16 | fix bug #2447 in congruence | Pierre Corbineau | |
| 2014-12-16 | fix bug #2447 in congruence | Pierre Corbineau | |
| 2014-12-16 | Fixing CAMLP4 compilation. | Pierre-Marie Pédrot | |
| 2014-12-16 | msg_info now puts infomsg tag in emacs mode. | Pierre Courtieu | |
| Fixes the idtac "string" not appearing in proofgeneral because printined *before* the goal. | |||
| 2014-12-16 | Proper thread-safe implementation for Exninfo. | Pierre-Marie Pédrot | |
| This is the second part of the Exninfo patch. It introduces dependency in the Thread library in all Coq files. | |||
| 2014-12-16 | Getting rid of Exninfo hacks. | Pierre-Marie Pédrot | |
| Instead of modifying exceptions to wear additional information, we instead use a dedicated type now. All exception-using functions were modified to support this new type, in particular Future's fix_exn-s and the tactic monad. To solve the problem of enriching exceptions at raise time and recover this data in the try-with handler, we use a global datastructure recording the given piece of data imperatively that we retrieve in the try-with handler. We ensure that such instrumented try-with destroy the data so that there may not be confusion with another exception. To further harden the correction of this structure, we also check for pointer equality with the last raised exception. The global data structure is not thread-safe for now, which is incorrect as the STM uses threads and enriched exceptions. Yet, we splitted the patch in two parts, so that we do not introduce dependencies to the Thread library immediatly. This will allow to revert only the second patch if ever we switch to OCaml-coded lightweight threads. | |||
| 2014-12-16 | Error messages of Searchxxx are coherent with goal selector. | Pierre Courtieu | |
| 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. | |||
| 2014-12-16 | Fix for #3154: use CUnix.sys_command to call native compiler. | Maxime Dénès | |
| 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. | |||
| 2014-12-15 | Changed bullet informations to warning for better display in PG. | Pierre Courtieu | |
| Since it displays together with the goal, it is better (for pg and other interfaces probably) that they are in a different message. | |||
| 2014-12-15 | Adapted test file for About. | Pierre Courtieu | |
| 2014-12-15 | Tentatively starting to use heuristics for evar-evar resolution: first | Hugo Herbelin | |
| 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. | |||
| 2014-12-15 | Failing on unbound notation variable in notation level modifiers | Hugo Herbelin | |
| + 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). | |||
| 2014-12-15 | New try on Fixing an evar_map bug revealed by commit 603b66f81 on | Hugo Herbelin | |
| unification flags (see also temporary revert in d083200ae5b). | |||
| 2014-12-15 | Tests for #3848 and #3854. | Hugo Herbelin | |
| 2014-12-15 | Documenting check_record + changing a possibly undefined int into int option. | Hugo Herbelin | |
| 2014-12-15 | About now accepts hypothesis names and goal selector. | Pierre Courtieu | |
| 2014-12-15 | Fix treatment of universe context in typecheck inductive (was added | Matthieu Sozeau | |
| twice). Thanks to Marc Lasson for spotting this. | |||
| 2014-12-15 | Tests for Searchxxx commands added and modified. | Pierre Courtieu | |
| 2014-12-15 | Fixing bug #3865. | Pierre-Marie Pédrot | |
| 2014-12-14 | Util.un_op -> Option.default | Pierre Boutillier | |
| 2014-12-14 | Fix merging of name maps in union of universe contexts. | Matthieu Sozeau | |
| 2014-12-14 | Fixing bug #3858 and #3817 in one stroke. | Pierre-Marie Pédrot | |
| 2014-12-14 | Revert "Fixing bug #3817." | Pierre-Marie Pédrot | |
| This reverts commit ad2a0308b1592c7235714a2cca926f3b55accbb2. | |||
| 2014-12-12 | Add Ltac syntax for the [tclIFCATCH] primitive. | Arnaud Spiwack | |
| [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. | |||
| 2014-12-12 | Make sure the goals on the shelve are identified as goal and unresolvable ↵ | Arnaud Spiwack | |
| 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. | |||
| 2014-12-12 | Searchxxx now interpret patterns in goal environment if any. | Pierre Courtieu | |
| This makes such things work: x:nat h: x = 3 ================ True Search x. | |||
| 2014-12-12 | #4843 part 2 : The .cmxs files for plug-ins must have execute permission | Pierre Boutillier | |
| 2014-12-12 | Fix #3163 and #3843 part 1 : Cygwin DLLs have extension ".so", not ".dll" | Pierre Boutillier | |
| 2014-12-12 | Fix #3800 : cmxs need execution priviledges under windows | Pierre Boutillier | |
| 2014-12-12 | An option SimplIsCbn | Pierre Boutillier | |
| 2014-12-12 | Extend the syntax of simpl with a delta flag. | Arnaud Spiwack | |
| You can write 'simpl -[plus minus] div2'. Simpl does not use it for now. | |||
| 2014-12-12 | Searchxxx now search also the hypothesis and support goal selector. | Pierre Courtieu | |
| Documentation also updated. | |||
| 2014-12-12 | Two fixes in unification (bugs #3782 and #3709) | Matthieu Sozeau | |
| - 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. | |||
| 2014-12-12 | In discrimination nets, do not index lambdas if they're part of a beta | Matthieu Sozeau | |
| redex. | |||
| 2014-12-11 | handling Functional Scheme for required but not imported modules | Julien Forest | |
| 2014-12-11 | List.v: sequel to Sebastien's commit (some cosmetics + a few shorter proofs) | Pierre Letouzey | |
| 2014-12-11 | First series of results on lists. | Sébastien Hinderer | |
| 2014-12-11 | Commit not ready. Sorry. | Hugo Herbelin | |
| Revert "Fixing an evar_map bug revealed by commit 603b66f81 on unification flags." This reverts commit d083200ae5b391ceffaa0329a8e3a334036c7968. | |||
| 2014-12-11 | Added a CannotSolveConstraint unification error and made experiments | Hugo Herbelin | |
| in reporting the chain of causes when unification fails. | |||
| 2014-12-11 | Fine-tuning unification error (using OccurCheck in evarconv). | Hugo Herbelin | |
| 2014-12-11 | Tentatively more informative report of failure when inferring | Hugo Herbelin | |
| pattern-matching predicate. | |||
| 2014-12-11 | Fixing an evar_map bug revealed by commit 603b66f81 on unification flags. | Hugo Herbelin | |
| This fixes current failure of RelationAlgebra. | |||
| 2014-12-11 | Test suite: keep message in sync with actual file deletions. | Xavier Clerc | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |