aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Collapse)Author
2017-05-22romega: if it bugs again, at least do it with a short and quick errorPierre Letouzey
2017-05-22refl_omega: comment the lack of lifts when dealing with arrowsPierre Letouzey
2017-05-22romega: 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-22refl_omega: more refactoring (e.g. IntSets instead of sorted lists)Pierre Letouzey
2017-05-22refl_omega: refactoring (e.g. useless args in destructurate_pos_hyp)Pierre Letouzey
2017-05-22ReflOmegaCore: discard useless cosntructor P_NOPPierre Letouzey
2017-05-22ReflOmegaCore: revised proofs (mostly bullets instead of ;[|||])Pierre Letouzey
2017-05-18Add .dir-locals.el to pluginsJason Gross
As requested in https://github.com/coq/coq/pull/386#issuecomment-302358542
2017-05-17Merge PR#633: An extension of EXTEND and notations to make standard parsing ↵Maxime Dénès
tricks available to users
2017-05-17Merge PR#607: Make congruence reuse discriminate instead of rolling its own.Maxime Dénès
2017-05-16Fixing grammar for "evar" by exporting the test_lpar_id_colon trick to EXTEND.Hugo Herbelin
2017-05-16Adding support for using grammar entries returning no value in EXTEND.Hugo Herbelin
2017-05-13Typo in a comment of plugin Quote.Hugo Herbelin
2017-05-11Merge PR#201: Transparent abstractMaxime Dénès
2017-05-09Merge PR#612: Set Ltac Batch DebugMaxime Dénès
2017-05-09Prevent user-defined ring morphisms from ever being evaluated.Guillaume Melquiond
2017-05-04Adding an option "Set Ltac Batch Debug" to additionally run Ltac debug in ↵Hugo Herbelin
batch mode.
2017-05-03Make 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-27Post-rebase warnings (unused opens and 2 unused values)Gaetan Gilbert
2017-04-27Fix 4.04 warningsGaetan Gilbert
2017-04-27Remove unused [open] statementsGaetan Gilbert
2017-04-27Micromega: do not use Filename.temp_dir_path, remove unused valuesGaetan Gilbert
2017-04-27Remove unused constructorsGaetan Gilbert
2017-04-27Add [_] prefix to unused values which maybe should be keptGaetan Gilbert
2017-04-27Remove some unused values and typesGaetan Gilbert
2017-04-27Rename Sos_lib.(||) -> parser_or to avoid (deprecated) Pervasives.orGaetan Gilbert
2017-04-27Disambiguate Polynomial.Hyp and Mfourier.Hyp -> AssumGaetan Gilbert
2017-04-27Fix omitted labels in function callsGaetan Gilbert
2017-04-27Remove unused [rec] keywordsGaetan Gilbert
2017-04-27Merge PR#568: Remove tactic compatibility layerMaxime Dénès
2017-04-25Add transparent_abstract tacticJason Gross
2017-04-25Merge PR#578: Fix nsatz not recognizing real literals.Maxime Dénès
2017-04-24Removing various tactic compatibility layers in core tactics.Pierre-Marie Pédrot
2017-04-24Porting the firstorder plugin to the new tactic API.Pierre-Marie Pédrot
2017-04-24Removing tactic compatibility layer in congruence.Pierre-Marie Pédrot
2017-04-24Removing tactic compatibility layer in Micromega.Pierre-Marie Pédrot
2017-04-24Fix 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-24Removing trivial compatibility layer in refl_omega.Pierre-Marie Pédrot
2017-04-24Porting omega to the new tactic API.Pierre-Marie Pédrot
2017-04-24Removing trivial compatibility layer in omega.Pierre-Marie Pédrot
2017-04-24Merge PR#579: [flags] Deprecate is_silent/is_verbose in favor of single flag.Maxime Dénès
2017-04-24Merge PR#565: Remove VernacErrorMaxime Dénès
2017-04-22Merge branch v8.6 into trunkHugo 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-21Remove VernacErrorGaetan 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-20Fix nsatz not recognizing real literals.Guillaume Melquiond
2017-04-15Merge branch 'v8.6' into trunkMaxime Dénès
2017-04-13Silence a few OCaml warnings.Guillaume Melquiond
2017-04-12Merge PR#441: Port Toplevel to the Stm APIMaxime 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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-31 09:02:25 +0000