aboutsummaryrefslogtreecommitdiff
path: root/toplevel/auto_ind_decl.ml
AgeCommit message (Expand)Author
2017-02-15[stm] Break stm/toplevel dependency loop.Emilio Jesus Gallego Arias
2017-02-01Merge branch 'v8.6'Pierre-Marie Pédrot
2017-01-23Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-12-23Excluding explicitly coinductive types in Scheme Equality (#5284).Hugo Herbelin
2016-12-22Fixing #5277 (Scheme Equality not robust wrt choice of names).Hugo Herbelin
2016-12-22Fixing anomaly EqUnknown in Equality Scheme (#5278).Hugo Herbelin
2016-10-02Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-02Fix bug #5069: Scheme Equality gives anomalies in sections.Pierre-Marie Pédrot
2016-09-08Merge PR #244.Pierre-Marie Pédrot
2016-08-24CLEANUP: minor readability improvementsMatej Kosik
2016-08-19Make the user_err header an optional parameter.Emilio Jesus Gallego Arias
2016-08-19Remove errorlabstrm in favor of user_errEmilio Jesus Gallego Arias
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-02-15merging conflicts with the original "trunk__CLEANUP__Context__2" branchMatej Kosik
2016-02-15Moving conversion functions to the new tactic API.Pierre-Marie Pédrot
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-21Stronger invariants on the use of the introduction pattern (pat1,...,patn).Hugo Herbelin
2016-01-20Update copyright headers.Maxime Dénès
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2015-12-05Moving extended_rel_vect/extended_rel_list to the kernel.Hugo Herbelin
2015-10-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-28Avoid type checking private_constants (side_eff) again during Qed (#4357).Enrico Tassi
2015-10-20Boxing the Goal.enter primitive into a record type.Pierre-Marie Pédrot
2015-10-02Fix after rebase...Matthieu Sozeau
2015-10-02Univs: fix environment handling in scheme building.Matthieu Sozeau
2015-09-23Hopefully better names to constructors of internal_flag, as discussedHugo Herbelin
2015-09-23Give a way to control if the decidable-equality schemes are built likeHugo Herbelin
2015-09-23Removing the generalization of the body of inductive schemes fromHugo Herbelin
2015-08-02Reverting 16 last commits, committed mistakenly using the wrong push command.Hugo Herbelin
2015-08-02Give a way to control if the decidable-equality schemes are built likeHugo Herbelin
2015-08-02Removing the generalization of the body of inductive schemes fromHugo Herbelin
2015-07-27Fixing bug #3736 (anomaly instead of error/warning/silence onHugo Herbelin
2015-05-13Safer typing primitives.Pierre-Marie Pédrot
2015-04-23Remove almost all the uses of string concatenation when building error messages.Guillaume Melquiond
2015-04-23Using tclZEROMSG instead of tclZERO in several places.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-11-13Fixing Scheme Equality, after bug introduced in bf018569405c.Hugo Herbelin
2014-10-25This commit introduces changes in induction and destruct.Hugo Herbelin
2014-09-06Renaming goal-entering functions.Pierre-Marie Pédrot
2014-08-18Reorganisation of intropattern codeHugo Herbelin
2014-08-18Reorganization of tactics:Hugo Herbelin
2014-08-05Experimentally adding an option for automatically erasing anHugo Herbelin
2014-06-18Proofs now take and return an evar_universe_context, simplifying interfacesMatthieu Sozeau
2014-05-08Renaming new_induct -> induction; new_destruct -> destruct.Hugo Herbelin
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-25Removing useless try-with clauses in Goal.enter variants.Pierre-Marie Pédrot
2014-03-31Removing dead code in Tactics.Pierre-Marie Pédrot
2014-03-26Adding a tclEFFECTS primitive allowing to push STM side-effects in tactics.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 15:35:01 +0000