aboutsummaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2018-10-02Fix deprecation warnings.Pierre-Marie Pédrot
2018-09-11Merge remote-tracking branch 'herbelin/master+globenv-coq-pr7288'Pierre-Marie Pédrot
2018-07-23Adding environment-manipulating functions.Pierre-Marie Pédrot
2018-07-23Fix deprecated warnings from Pcoq.Pierre-Marie Pédrot
2018-07-23Merge remote-tracking branch 'origin/pr/54'Pierre-Marie Pédrot
2018-07-04Adapting to move of register_constr_interp0 from Pretyping to GlobEnv.Hugo Herbelin
2018-06-23Fix for compilation with the camlp5-parser branch.Pierre-Marie Pédrot
2018-06-18Adapt to Coq's PR #7797 (removal of reference).Maxime Dénès
2018-06-18Do not rely on the Ident vs. Qualid artificial separation.Pierre-Marie Pédrot
2018-06-18Fixing a batch of deprecation warnings.Pierre-Marie Pédrot
2018-05-30Merge pull request coq/ltac2#60 from ejgallego/vernac+move_parserPierre-Marie Pédrot
2018-05-28Fix w.r.t. coq/coq#7521.Pierre-Marie Pédrot
2018-05-27Adapt to coq/coq#7558.Emilio Jesus Gallego Arias
2018-05-25Renaming global_reference according to Coq PR #6156.Hugo Herbelin
2018-05-25Renaming smartmap and fold_map according to Coq PR #7177.Hugo Herbelin
2018-05-24Adapt to fix/cofix changes in Coq (coq/coq#7196)Emilio Jesus Gallego Arias
2018-04-19Allowing formatting break around a printed type.Hugo Herbelin
2018-04-19Fixing printing level for subtypes of a type constructor.Hugo Herbelin
2018-04-11Fix compilation w.r.t. coq/coq#7213.Pierre-Marie Pédrot
2018-04-02[coq] Adapt to coq/coq#6960.Emilio Jesus Gallego Arias
2018-03-27Fix printing of toplevel record values.Pierre-Marie Pédrot
2018-03-27Fixup strict mode for patternsPierre-Marie Pédrot
2018-03-10Merge pull request coq/ltac2#46 from ejgallego/located+libnamesPierre-Marie Pédrot
2018-03-10Merge pull request coq/ltac2#47 from ejgallego/ssr+correct_packingPierre-Marie Pédrot
2018-03-10[coq] Adapt to coq/coq#6837.Emilio Jesus Gallego Arias
2018-03-10[coq] Adapt to coq/coq#6831.Emilio Jesus Gallego Arias
2018-03-09Fix compilation after the change of API in options.Pierre-Marie Pédrot
2018-03-05[coq] Adapt to correct LTAC module packing coq/coq#6869Emilio Jesus Gallego Arias
2018-03-01[coq] Adapt to coq/coq#6511Emilio Jesus Gallego Arias
2018-03-01[api] Remove some deprecation warnings.Emilio Jesus Gallego Arias
2018-02-27Merge remote-tracking branch 'origin/pr/44'Pierre-Marie Pédrot
2018-02-14adapt to Coq#6676Enrico Tassi
2018-02-14[coq] Adapt to coq/coq#6745Emilio Jesus Gallego Arias
2017-12-26adapt to API.mli removalEnrico Tassi
2017-12-08Adapt to removal of match_appsubterm.Théo Zimmermann
2017-11-24A possible fix after PR#6158 (raw/glob generic printers for ltac values).Hugo Herbelin
2017-11-21[coq] Adapt to Coq's new functional EXTEND API.Emilio Jesus Gallego Arias
2017-11-06Generalize the use of repr in Tac2stdlib.Pierre-Marie Pédrot
2017-11-04A possible fix after PR#6047 (a generic printer for ltac values).Hugo Herbelin
2017-11-02Factorizing entries for patterns with type constraints.Pierre-Marie Pédrot
2017-11-02Moving pattern type constraints to pattern AST.Pierre-Marie Pédrot
2017-11-02Binding the specialize tactic.Pierre-Marie Pédrot
2017-10-30Put notations in level 5 by default.Pierre-Marie Pédrot
2017-10-30Fix the semantics of introducing with empty intro patterns.Pierre-Marie Pédrot
2017-10-30Introducing the change tactic.Pierre-Marie Pédrot
2017-10-30Fix compilation after merge of Ltac_pretype interface.Pierre-Marie Pédrot
2017-10-27Better printers for toplevel values.Pierre-Marie Pédrot
2017-10-27Adding a command to evaluate Ltac2 expressions.Pierre-Marie Pédrot
2017-10-27Fix goal_matching quotation.Pierre-Marie Pédrot
2017-10-27Fix relative meaning of Pattern vs. Context in match goal.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-27 02:51:20 +0000