| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2017-04-24 | [location] Move Glob_term.cases_pattern to located. | Emilio Jesus Gallego Arias | |
| We continue the uniformization pass. No big news here, trying to be minimally invasive. | |||
| 2017-04-24 | [location] Use Loc.located for constr_expr. | Emilio Jesus Gallego Arias | |
| This is the second patch, which is a bit more invasive. We reasoning is similar to the previous patch. Code is not as clean as it could as we would need to convert `glob_constr` to located too, then a few parts could just map the location. | |||
| 2017-04-24 | [constrexpr] Make patterns use Loc.located for location information | Emilio Jesus Gallego Arias | |
| This is first of a series of patches, converting `constrexpr` pattern data type from ad-hoc location handling to `Loc.located`. Along Coq, we can find two different coding styles for handling objects with location information: one style uses `'a Loc.located`, whereas other data structures directly embed `Loc.t` in their constructors. Handling all located objects uniformly would be very convenient, and would allow optimizing certain cases, in particular making located smarter when there is no location information, as it is the case for all terms coming from the kernel. `git grep 'Loc.t \*'` gives an overview of the remaining work to do. We've also added an experimental API for `located` to the `Loc` module, `Loc.tag` should be used to add locations objects, making it explicit in the code when a "located" object is created. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |