| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | 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 | |
| 2017-04-07 | [camlpX] Remove camlp4 compat layer. | Emilio Jesus Gallego Arias | |
| We remove the camlp4 compatibility layer, and try to clean up most structures. `parsing/compat` is gone. We added some documentation to the lexer/parser interfaces that are often obscured by module includes. | |||
| 2017-04-06 | Merge PR#455: Farewell decl_mode | Maxime Dénès | |
| 2017-04-06 | Merge PR#508: Optimize pending evars | Maxime Dénès | |
| 2017-04-06 | Fix a normalization hotspot in computation of constr keys. | Pierre-Marie Pédrot | |
| Getting a key only needs to observe the root of a term. This hotspot was observed in HoTT. | |||
| 2017-04-04 | end of correction of bug 4306 | Julien Forest | |
| 2017-04-04 | Bad correction in previous commit | Julien Forest | |
| 2017-04-04 | Solving first problem in bug #4306. TO DO : solve the let in problem | Julien Forest | |
| 2017-04-04 | Merge branch 'trunk' into pr379 | Maxime Dénès | |
| 2017-04-03 | Merge PR#417: No cast surgery in let in | Maxime Dénès | |
| 2017-04-01 | Using delayed universe instances in EConstr. | Pierre-Marie Pédrot | |
| The transition has been done a bit brutally. I think we can still save a lot of useless normalizations here and there by providing the right API in EConstr. Nonetheless, this is a first step. | |||
| 2017-04-01 | Declaring ltac plugin, so that static linking works. | Hugo Herbelin | |
| 2017-04-01 | Actually exporting delayed universes in the EConstr implementation. | Pierre-Marie Pédrot | |
| For now we only normalize sorts, and we leave instances for the next commit. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |