aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Collapse)AuthorAge
...
| * | Remove unused constructorsGravatar Gaetan Gilbert2017-04-27
| | |
| * | Add [_] prefix to unused values which maybe should be keptGravatar Gaetan Gilbert2017-04-27
| | |
| * | Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
| | |
| * | Rename Sos_lib.(||) -> parser_or to avoid (deprecated) Pervasives.orGravatar Gaetan Gilbert2017-04-27
| | |
| * | Disambiguate Polynomial.Hyp and Mfourier.Hyp -> AssumGravatar Gaetan Gilbert2017-04-27
| | |
| * | Fix omitted labels in function callsGravatar Gaetan Gilbert2017-04-27
| | |
| * | Remove unused [rec] keywordsGravatar Gaetan Gilbert2017-04-27
| | |
| * | Merge PR#568: Remove tactic compatibility layerGravatar Maxime Dénès2017-04-27
| |\ \
| | | * Add transparent_abstract tacticGravatar Jason Gross2017-04-25
| | |/ | |/|
| * | Merge PR#578: Fix nsatz not recognizing real literals.Gravatar Maxime Dénès2017-04-25
| |\ \
* | | | [location] [ast] Port module AST to CAstGravatar Emilio Jesus Gallego Arias2017-04-25
| | | |
* | | | [location] [ast] Switch Constrexpr AST to an extensible node type.Gravatar Emilio Jesus Gallego Arias2017-04-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | [location] Remove `Loc.internal_ghost`Gravatar Emilio Jesus Gallego Arias2017-04-25
| | | | | | | | | | | | | | | | | | | | `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.
* | | | [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
| | | | | | | | | | | | | | | | Now it is a private field, locations are optional.
* | | | [location] Use located in tactics.Gravatar Emilio Jesus Gallego Arias2017-04-24
| | | | | | | | | | | | | | | | One case missing due the TACTIC EXTEND macro.
* | | | [location] Use located in misctypes.Gravatar Emilio Jesus Gallego Arias2017-04-24
| | | |
* | | | [location] Switch glob_constr to Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-24
| | | |
* | | | [location] Move Glob_term.cases_pattern to located.Gravatar Emilio Jesus Gallego Arias2017-04-24
| | | | | | | | | | | | | | | | | | | | We continue the uniformization pass. No big news here, trying to be minimally invasive.
* | | | [location] Use Loc.located for constr_expr.Gravatar Emilio Jesus Gallego Arias2017-04-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | [constrexpr] Make patterns use Loc.located for location informationGravatar Emilio Jesus Gallego Arias2017-04-24
|/ / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | * Removing various tactic compatibility layers in core tactics.Gravatar Pierre-Marie Pédrot2017-04-24
| | |
| | * Porting the firstorder plugin to the new tactic API.Gravatar Pierre-Marie Pédrot2017-04-24
| | |
| | * Removing tactic compatibility layer in congruence.Gravatar Pierre-Marie Pédrot2017-04-24
| | |
| | * Removing tactic compatibility layer in Micromega.Gravatar Pierre-Marie Pédrot2017-04-24
| | |
| | * Fix the API of the new pf_constr_of_global.Gravatar Pierre-Marie Pédrot2017-04-24
| | | | | | | | | | | | | | | | | | 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.
| | * Removing trivial compatibility layer in refl_omega.Gravatar Pierre-Marie Pédrot2017-04-24
| | |
| | * Porting omega to the new tactic API.Gravatar Pierre-Marie Pédrot2017-04-24
| | |
| | * Removing trivial compatibility layer in omega.Gravatar Pierre-Marie Pédrot2017-04-24
| |/ |/|
* | Merge PR#579: [flags] Deprecate is_silent/is_verbose in favor of single flag.Gravatar Maxime Dénès2017-04-24
|\ \
* \ \ Merge PR#565: Remove VernacErrorGravatar Maxime Dénès2017-04-24
|\ \ \
* \ \ \ Merge branch v8.6 into trunkGravatar Hugo Herbelin2017-04-22
|\ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | * | | Remove VernacErrorGravatar Gaetan Gilbert2017-04-21
| |/ / / |/| | |
| | * | [flags] Deprecate is_silent/is_verbose in favor of single flag.Gravatar Emilio Jesus Gallego Arias2017-04-21
| |/ / |/| | | | | | | | | | | | | | | | | | | | | | | 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.
| | * Fix nsatz not recognizing real literals.Gravatar Guillaume Melquiond2017-04-20
| |/ |/|
* | Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-04-15
|\ \
* | | Silence a few OCaml warnings.Gravatar Guillaume Melquiond2017-04-13
| | |
* | | Merge PR#441: Port Toplevel to the Stm APIGravatar Maxime Dénès2017-04-12
|\ \ \
| * | | [stm] Remove edit_id.Gravatar Emilio Jesus Gallego Arias2017-04-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of ↵Gravatar Maxime Dénès2017-04-12
|\ \ \ \ | | | | | | | | | | | | | | | record fields.
* \ \ \ \ Merge PR#532: Clean Nsatz implementation.Gravatar Maxime Dénès2017-04-11
|\ \ \ \ \
* \ \ \ \ \ Merge PR#379: Introducing evar-insensitive constrsGravatar Maxime Dénès2017-04-11
|\ \ \ \ \ \ | |_|_|/ / / |/| | | | |
| | * | | | Fix an algorithmic issue in Nsatz.Gravatar Pierre-Marie Pédrot2017-04-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | * | | | Academic prescriptivism strikes back: down with baroque programming in Nsatz.Gravatar Pierre-Marie Pédrot2017-04-09
| |/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * | | | Fix an unhandled exception in Omega.Gravatar Pierre-Marie Pédrot2017-04-07
| | | | |
| * | | | Merge branch 'master' into econstrGravatar Pierre-Marie Pédrot2017-04-07
| |\ \ \ \
* | | | | | [camlpX] Remove camlp4 compat layer.Gravatar Emilio Jesus Gallego Arias2017-04-07
| |/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | | Merge PR#455: Farewell decl_modeGravatar Maxime Dénès2017-04-06
|\ \ \ \ \
* \ \ \ \ \ Merge PR#508: Optimize pending evarsGravatar Maxime Dénès2017-04-06
|\ \ \ \ \ \
| | | * | | | Fix a normalization hotspot in computation of constr keys.Gravatar Pierre-Marie Pédrot2017-04-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Getting a key only needs to observe the root of a term. This hotspot was observed in HoTT.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 15:05:03 +0000