| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-05-09 | Adjusting test-suite after 5cbc018fe9347 (subst as in 8.4 by default). | Hugo Herbelin | |
| 2015-05-09 | Adding a flag "Set Regular Subst Tactic" off by default in v8.5 for | Hugo Herbelin | |
| preserving compatibility of subst after #4214 being solved. | |||
| 2015-05-06 | Fixing treatment of recursive equations damaged by 857e82b2ca0d1. | Hugo Herbelin | |
| Improving treatment of recursive equations compared to 8.4 (see test-suite). Experimenting not to unfold local defs ever in subst. (+ Slight simplification in checking reflexive equalities only once). | |||
| 2015-05-05 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-05-01 | Fixing computation of implicit arguments by position in fixpoints (#4217). | Hugo Herbelin | |
| 2015-05-01 | Giving to "subst" a more natural semantic (fixing #4214) by using all | Hugo Herbelin | |
| equalities in configurations like x=y x=z === P(x,y,z) where it now produces === P(z,z,z) In particular (equations are processed from most ancient to most recent). Thanks to this, a "repeat subst" can just be a "subst" in List.v. Incidentally: moved a nf_enter to enter in subst_one, since the latter is normally called from other tactics having normalized evars. | |||
| 2015-04-22 | Tactical `progress` compares term up to potentially equalisable universes. | Arnaud Spiwack | |
| Followup of: f7b29094fe7cc13ea475447bd30d9a8b942f0fef . In particular, re-closes #3593. As a side effect, fixes an undiscovered bug of the `eq_constr` tactic which didn't consider terms up to evar instantiation. | |||
| 2015-04-22 | Test for #4198 (appcontext in return clause of match). | Hugo Herbelin | |
| 2015-04-21 | Fixing #3376 and #4191 (wrong index of maximally-inserted implicit argument | Hugo Herbelin | |
| in the presence of let-ins). | |||
| 2015-04-17 | Extra fix to 934761875 and f4ee7ee31e4 on optimizing Import of several | Hugo Herbelin | |
| libraries at once (see #4193). | |||
| 2015-04-16 | Test for bug #4190. | Pierre-Marie Pédrot | |
| 2015-04-15 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-04-10 | Test for bug #3199. | Pierre-Marie Pédrot | |
| 2015-04-09 | Better test-suite files, removing reliance on admit. | Matthieu Sozeau | |
| 2015-04-09 | Fix declarations of instances to perform restriction of universe | Matthieu Sozeau | |
| instances as definitions and lemmas do (fixes bug# 4121). | |||
| 2015-04-09 | Add test-suite file for bug #4120. | Matthieu Sozeau | |
| 2015-04-09 | Merge branch 'v8.5' into trunk | Pierre Letouzey | |
| 2015-04-06 | Test for bug #3815. | Pierre-Marie Pédrot | |
| 2015-04-01 | Fixing test-suite. | Pierre-Marie Pédrot | |
| 2015-03-31 | Fixing test-suite. | Pierre-Marie Pédrot | |
| 2015-03-30 | Merge branch 'v8.5' into trunk | Enrico Tassi | |
| 2015-03-30 | camlp4: grep away warnings in output/* tests | Enrico Tassi | |
| 2015-03-29 | Adding test for bug #4165. | Pierre-Marie Pédrot | |
| 2015-03-25 | Fully fixing bug #3491 (anomaly when building _rect scheme in the | Hugo Herbelin | |
| presence of let-ins and recursively non-uniform parameters). The bug was in the List.chop of Inductiveops.get_arity which was wrong in the presence of let-ins and recursively non-uniform parameters. The bug #3491 showed up because, in addition to have let-ins, it was wrongly detected as having recursively non-uniform parameters. Also added some comments in declarations.mli. | |||
| 2015-03-25 | Another example about the consequence of a wrong computation of the | Hugo Herbelin | |
| number of recursively uniform parameters in the presence of let-ins. In practice, more recursively non-uniform parameters were assumed and this was used especially for checking positivity of nested types, leading to refusing more nested types than necessary (see Inductive.v). | |||
| 2015-03-24 | Updating test-suite (see previous commit). | Hugo Herbelin | |
| 2015-03-24 | Fixing computation of non-recursively uniform arguments in the | Hugo Herbelin | |
| presence of let-ins. This fixes #3491. | |||
| 2015-03-24 | Fixing wrong rel_context in checking positivity condition. | Hugo Herbelin | |
| Parameters were missing in the context, apparently without negative effects because the context was used only for whd normalization of types, while reduction (in closure.ml) was resistant to unbound rels. See however next commit for an indirect effect on the wrong computation of non recursively uniform parameters producing an anomaly when computing _rect schemas. | |||
| 2015-03-23 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-03-22 | Qed export -> Qed exporting | Enrico Tassi | |
| 2015-03-13 | Merge branch 'v8.5' into trunk | Arnaud Spiwack | |
| 2015-03-13 | Add some tests for tryif | Jason Gross | |
| + adjusting for the removal of `admit` by Arnaud Spiwack. | |||
| 2015-03-11 | Fix regression in HoTT_coq_014.v | Enrico Tassi | |
| Admitted was not using the partial proof to infer discharged variables. Now it does. The fix makes no sense, but restore the old behavior. | |||
| 2015-03-11 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-03-11 | admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032) | Enrico Tassi | |
| - no more inconsistent Axiom in the Prelude - STM can now process Admitted proofs asynchronously - the quick chain can stock "Admitted" jobs in .vio files - the vio2vo step checks the jobs but does not stock the result in the opaque tables (they have no slot) - Admitted emits a warning if the proof is complete - Admitted uses the (partial) proof term to infer section variables used (if not given with Proof using), like for Qed - test-suite: extra line Require TestSuite.admit to each file making use of admit - test-suite/_CoqProject: to pass to CoqIDE and PG the right -Q flag to find TestSuite.admit | |||
| 2015-03-09 | Do not display the status of monomorphic constants unless in ↵ | Guillaume Melquiond | |
| universe-polymorphism mode. | |||
| 2015-03-08 | Test for bug #2951. | Pierre-Marie Pédrot | |
| 2015-03-07 | Test for #4035 (dependent destruction from Ltac). | Hugo Herbelin | |
| 2015-03-06 | Merge branch 'v8.5' into trunk | Pierre Letouzey | |
| 2015-03-05 | Fix testsuite with respect to the new formatting of Fail messages. | Guillaume Melquiond | |
| 2015-03-04 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-03-03 | Fix test-suite file, this is open. | Matthieu Sozeau | |
| 2015-03-03 | Fix bug #3732: firstorder was using detyping to build existential | Matthieu Sozeau | |
| instances and forgeting about the evars and universes that could appear there... dirty hack gone, using the evar map properly and avoiding needless constructions/deconstructions of terms. | |||
| 2015-03-03 | Add missing test-suite files and update gitignore. | Matthieu Sozeau | |
| 2015-03-03 | Add a test-suite file ensuring coinductives with primitive projections | Matthieu Sozeau | |
| do not enjoy eta-conversion and do not allow the usual failure of subject reduction in presence of dependent pattern-matching. | |||
| 2015-03-03 | Fix test-suite file, this is currently a wontfix, but keep the | Matthieu Sozeau | |
| test-suite file for when we move to a better implementation. | |||
| 2015-03-03 | Fix bug #4103: forgot to allow unfolding projections of cofixpoints like | Matthieu Sozeau | |
| cases, in some cases. | |||
| 2015-03-03 | Fix bug #4101, noccur_evar's expand_projection can legitimately fail | Matthieu Sozeau | |
| when called from w_unify, so we protect it. | |||
| 2015-03-02 | Fix bug #4097. | Matthieu Sozeau | |
| 2015-02-28 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |
path: root/test-suite