| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | 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-24 | Removing various tactic compatibility layers in core tactics. | Pierre-Marie Pédrot | |
| 2017-04-24 | Porting the firstorder plugin to the new tactic API. | Pierre-Marie Pédrot | |
| 2017-04-24 | Removing tactic compatibility layer in congruence. | Pierre-Marie Pédrot | |
| 2017-04-24 | Removing tactic compatibility layer in Micromega. | Pierre-Marie Pédrot | |
| 2017-04-24 | Fix the API of the new pf_constr_of_global. | Pierre-Marie Pédrot | |
| The current implementation was still using continuation passing-style, and furthermore was triggering a focus on the goals. We take advantage of the tactic features instead. | |||
| 2017-04-24 | Removing trivial compatibility layer in refl_omega. | Pierre-Marie Pédrot | |
| 2017-04-24 | Porting omega to the new tactic API. | Pierre-Marie Pédrot | |
| 2017-04-24 | Removing trivial compatibility layer in omega. | Pierre-Marie Pédrot | |
| 2017-04-24 | Merge PR#579: [flags] Deprecate is_silent/is_verbose in favor of single flag. | Maxime Dénès | |
| 2017-04-24 | Merge PR#565: Remove VernacError | Maxime Dénès | |
| 2017-04-22 | Merge branch v8.6 into trunk | Hugo Herbelin | |
| Note: I removed what seemed to be dead code in recdef.ml (local_assum and local_def introduced with econstr branch), assuming that this is what should be done. | |||
| 2017-04-21 | Remove VernacError | Gaetan Gilbert | |
| 2017-04-21 | [flags] Deprecate is_silent/is_verbose in favor of single flag. | Emilio Jesus Gallego Arias | |
| Today, both modes are controlled by a single flag, however this is a bit misleading as is_silent really means "quiet", that is to say `coqc -q` whereas "verbose" is Coq normal operation. We also restore proper behavior of goal printing in coqtop on quiet mode, thanks to @Matafou for the report. | |||
| 2017-04-20 | Fix nsatz not recognizing real literals. | Guillaume Melquiond | |
| 2017-04-15 | Merge branch 'v8.6' into trunk | Maxime Dénès | |
| 2017-04-13 | Silence a few OCaml warnings. | Guillaume Melquiond | |
| 2017-04-12 | Merge PR#441: Port Toplevel to the Stm API | Maxime Dénès | |
| 2017-04-12 | [stm] Remove edit_id. | Emilio Jesus Gallego Arias | |
| We remove `edit_id` from the STM. In PIDE they serve a different purpose, however in Coq they were of limited utility and required many special cases all around the code. Indeed, parsing is not an asynchronous operation in Coq, thus having feedback about parsing didn't make much sense. All clients indeed ignore such feedback and handle parsing in a synchronous way. XML protocol clients are unaffected, they rely on the instead on the Fail value. This commit supersedes PR#203. | |||
| 2017-04-12 | Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of ↵ | Maxime Dénès | |
| record fields. | |||
| 2017-04-11 | Merge PR#532: Clean Nsatz implementation. | Maxime Dénès | |
| 2017-04-11 | Merge PR#379: Introducing evar-insensitive constrs | Maxime Dénès | |
| 2017-04-09 | Fix an algorithmic issue in Nsatz. | Pierre-Marie Pédrot | |
| We use heaps instead of continuously adding elements to an ordered list, which was quadratic in the worst case. As a byproduct, this solves bug #5359, which was due to a stack overflow on big lists. | |||
| 2017-04-09 | Academic prescriptivism strikes back: down with baroque programming in Nsatz. | Pierre-Marie Pédrot | |
| Several cleanups were performed. 1. Removal of dead code lurking around. 2. Removal of global variables used to pass arguments to functions, as well as unnecessary mutable state here and there. We rely on state-passing and encapsulated mutable state. 3. Removal of crazy reference manipulation and its replacement with proper list handling, as well as cleaning up the source and taking advantage of invariants. This should solve algorithmic limitations of the previous code. 4. Opacification of some structures to have a clearer idea of the code requirements. 5. Cleaning of debug printing functions. We thunk the computation of the debugging data, whose computation can be costly for no reason, and we rely on Feedback-based interaction instead of Printf-debugging. | |||
| 2017-04-07 | Fix an unhandled exception in Omega. | Pierre-Marie Pédrot | |
| 2017-04-07 | Merge branch 'master' into econstr | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |