| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-05-22 | romega/const_omega : a few improvements (less try with, no gen equality) | Pierre Letouzey | |
| 2017-05-22 | romega: use N instead of nat for Tvar | Pierre Letouzey | |
| In a coming commit, we'll normalize terms by a Coq function that will compare Tvar's instead of blindly applying a trace, so let's speed-up these comparisons. | |||
| 2017-05-22 | romega: shorter trace (no more term lengths) | Pierre Letouzey | |
| 2017-05-22 | refl_omega: refactoring of normalize_equation | Pierre Letouzey | |
| 2017-05-22 | ReflOmegaCore: lots of dead code + a few refactored proofs | Pierre Letouzey | |
| 2017-05-22 | romega: if it bugs again, at least do it with a short and quick error | Pierre Letouzey | |
| 2017-05-22 | refl_omega: comment the lack of lifts when dealing with arrows | Pierre Letouzey | |
| 2017-05-22 | romega: discard constructor D_mono (shorter trace + fix a bug) | Pierre Letouzey | |
| For the bug, see new test test_romega10 in test-suite/success/ROmega0.v. | |||
| 2017-05-22 | refl_omega: more refactoring (e.g. IntSets instead of sorted lists) | Pierre Letouzey | |
| 2017-05-22 | refl_omega: refactoring (e.g. useless args in destructurate_pos_hyp) | Pierre Letouzey | |
| 2017-05-22 | ReflOmegaCore: discard useless cosntructor P_NOP | Pierre Letouzey | |
| 2017-05-22 | ReflOmegaCore: revised proofs (mostly bullets instead of ;[|||]) | Pierre Letouzey | |
| 2017-05-22 | Using type classes in the interpretation of "specialize" and "contradiction". | Hugo Herbelin | |
| We do that by using constr_with_bindings rather than open_constr_with_bindings (+ extra call to typeclasses in "specialize"). If my understanding is right, the only effect would be to succeed more in cases where it was failing (in inh_conv_coerce_to_gen). In particular, "specialize" and "contradiction" already have a WITHHOLES test for rejecting pending holes. Incidentally, this answers enhancement #5153. | |||
| 2017-05-22 | Clarifying the interpretation path for the "constr_with_binding" argument. | Hugo Herbelin | |
| This fixes an inconsistency introduced in 554a6c806 (svn r12603) where both interp_constr_with_bindings and interp_open_constr_with_bindings were going through interp_open_constr (no type classes so as to not to commit too early on irreversible choices, accepting unresolved holes). We fix this by having interp_constr_with_bindings going to interp_constr (using type classes and failing on unresolved evars). The external impact is that any TACTIC EXTEND which refers to constr_with_binding has now to decide whether it intends it to use what the name suggest (using type classes and to fail if evars remain unresolved), thus keeping constr_with_binding, or the actual behavior which requires to use open_constr_with_bindings for strict compatibility. | |||
| 2017-05-19 | Merge branch 'master' into ltac2-hooks | Pierre-Marie Pédrot | |
| 2017-05-18 | Add .dir-locals.el to plugins | Jason Gross | |
| As requested in https://github.com/coq/coq/pull/386#issuecomment-302358542 | |||
| 2017-05-17 | Merge PR#633: An extension of EXTEND and notations to make standard parsing ↵ | Maxime Dénès | |
| tricks available to users | |||
| 2017-05-17 | Merge PR#607: Make congruence reuse discriminate instead of rolling its own. | Maxime Dénès | |
| 2017-05-16 | Fixing grammar for "evar" by exporting the test_lpar_id_colon trick to EXTEND. | Hugo Herbelin | |
| 2017-05-16 | Adding support for using grammar entries returning no value in EXTEND. | Hugo Herbelin | |
| 2017-05-13 | Typo in a comment of plugin Quote. | Hugo Herbelin | |
| 2017-05-11 | Merge PR#201: Transparent abstract | Maxime Dénès | |
| 2017-05-09 | Merge PR#612: Set Ltac Batch Debug | Maxime Dénès | |
| 2017-05-09 | Prevent user-defined ring morphisms from ever being evaluated. | Guillaume Melquiond | |
| 2017-05-04 | Adding an option "Set Ltac Batch Debug" to additionally run Ltac debug in ↵ | Hugo Herbelin | |
| batch mode. | |||
| 2017-05-03 | Generalizing the tactic-in-term embedding to any generic argument. | Pierre-Marie Pédrot | |
| 2017-05-03 | Allowing to pass arbitrary data in internalization environments. | Pierre-Marie Pédrot | |
| 2017-05-03 | Make congruence reuse discriminate instead of rolling its own. | Gaetan Gilbert | |
| This changes the produced terms a bit, eg Axiom T : Type. Lemma foo : true = false -> T. Proof. congruence. Qed. used to produce fun H : true = false => let Heq := H : true = false in @eq_rect Type True (fun X : Type => X) I T (@f_equal bool Type (fun t : bool => if t then True else T) true false Heq) now produces fun H : true = false => let Heq : true = false := H in let H0 : False := @eq_ind bool true (fun e : bool => if e then True else False) I false Heq in False_rect T H0 i.e. instead of proving [True = T] by [f_equal] then transporting [I] across this identity, it now proves [False] by [eq_ind] then uses exfalso. | |||
| 2017-04-27 | Post-rebase warnings (unused opens and 2 unused values) | Gaetan Gilbert | |
| 2017-04-27 | Fix 4.04 warnings | Gaetan Gilbert | |
| 2017-04-27 | Remove unused [open] statements | Gaetan Gilbert | |
| 2017-04-27 | Micromega: do not use Filename.temp_dir_path, remove unused values | Gaetan Gilbert | |
| 2017-04-27 | Remove unused constructors | Gaetan Gilbert | |
| 2017-04-27 | Add [_] prefix to unused values which maybe should be kept | Gaetan Gilbert | |
| 2017-04-27 | Remove some unused values and types | Gaetan Gilbert | |
| 2017-04-27 | Rename Sos_lib.(||) -> parser_or to avoid (deprecated) Pervasives.or | Gaetan Gilbert | |
| 2017-04-27 | Disambiguate Polynomial.Hyp and Mfourier.Hyp -> Assum | Gaetan Gilbert | |
| 2017-04-27 | Fix omitted labels in function calls | Gaetan Gilbert | |
| 2017-04-27 | Remove unused [rec] keywords | Gaetan Gilbert | |
| 2017-04-27 | Merge PR#568: Remove tactic compatibility layer | Maxime Dénès | |
| 2017-04-25 | Add transparent_abstract tactic | Jason Gross | |
| 2017-04-25 | Merge PR#578: Fix nsatz not recognizing real literals. | Maxime Dénès | |
| 2017-04-25 | [location] [ast] Port module AST to CAst | Emilio Jesus Gallego Arias | |
| 2017-04-25 | [location] [ast] Switch Constrexpr AST to an extensible node type. | Emilio Jesus Gallego Arias | |
| Following @gasche idea, and the original intention of #402, we switch the main parsing AST of Coq from `'a Loc.located` to `'a CAst.ast` which is private and record-based. This provides significantly clearer code for the AST, and is robust wrt attributes. | |||
| 2017-04-25 | [location] Remove `Loc.internal_ghost` | Emilio Jesus Gallego Arias | |
| `internal_ghost` was an artifact to ease porting of the ml4 rules. Now that the location is optional we can finally get rid of it. | |||
| 2017-04-25 | [location] Make location optional in Loc.located | Emilio Jesus Gallego Arias | |
| This completes the Loc.ghost removal, the idea is to gear the API towards optional, but uniform, location handling. We don't print <unknown> anymore in the case there is no location. This is what the test suite expects. The old printing logic for located items was a bit inconsistent as it sometimes printed <unknown> and other times it printed nothing as the caller checked for `is_ghost` upstream. | |||
| 2017-04-25 | [location] Remove Loc.ghost. | Emilio Jesus Gallego Arias | |
| Now it is a private field, locations are optional. | |||
| 2017-04-24 | [location] Use located in tactics. | Emilio Jesus Gallego Arias | |
| One case missing due the TACTIC EXTEND macro. | |||
| 2017-04-24 | [location] Use located in misctypes. | Emilio Jesus Gallego Arias | |
| 2017-04-24 | [location] Switch glob_constr to Loc.located | Emilio Jesus Gallego Arias | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |