aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-01-04Extraction: msg_notice instead of msg_info.Pierre Courtieu
2016-01-04Fix handling of side-effects in case of `Opaque side-effects as well.Matthieu Sozeau
2016-01-04par: check if the goal is not ground and fail (fix #4465)Enrico Tassi
2016-01-04workers: purge short version of -load-vernac too (fix #4458)Enrico Tassi
2016-01-02Use streams rather than strings to handle bullet suggestions.Guillaume Melquiond
2016-01-02Remove some unused functions.Guillaume Melquiond
2016-01-02Remove keys for evar and meta, since they cannot occur.Guillaume Melquiond
2016-01-02Remove some useless type declarations.Guillaume Melquiond
2016-01-02Remove some useless module opening.Guillaume Melquiond
2016-01-02Remove duplicate definition.Guillaume Melquiond
2016-01-02Remove duplicate declarations.Guillaume Melquiond
2016-01-02Reduce dependencies of interface files.Guillaume Melquiond
2016-01-02Avoid warnings about loop indices.Guillaume Melquiond
2016-01-02Remove useless rec flags.Guillaume Melquiond
2016-01-02Simplification of grammar_prod_item type.Pierre-Marie Pédrot
2016-01-02Proper datatype for EXTEND syntax tokens.Pierre-Marie Pédrot
2016-01-02Separation of concern in TacAlias API.Pierre-Marie Pédrot
2016-01-01Fix typos.Guillaume Melquiond
2016-01-01Remove unused hashconsing code.Guillaume Melquiond
2016-01-01Do not make it harder on the compiler optimizer by packing arguments.Guillaume Melquiond
2016-01-01Remove unused functions.Guillaume Melquiond
2016-01-01Remove unplugged button from the interface.Guillaume Melquiond
2016-01-01Remove useless recursive flags.Guillaume Melquiond
2016-01-01Remove unused open.Guillaume Melquiond
2016-01-01Remove duplicate declarations.Guillaume Melquiond
2015-12-31Put implicits back as in 8.4.Matthieu Sozeau
2015-12-31Fix bug #4456, anomaly in handle-side effectsMatthieu Sozeau
2015-12-31Remove unused function Checker.print_loc.Guillaume Melquiond
2015-12-31Merge branch 'v8.5' into trunkGuillaume Melquiond
2015-12-31Do not compose List.length with List.filter.Guillaume Melquiond
2015-12-31Remove Library.mem, which is pointless since 8.5.Guillaume Melquiond
2015-12-31Do not dump a glob reference when its location is ghost. (Fix bug #4469)Guillaume Melquiond
2015-12-30Moving apply_type to new proof engine.Hugo Herbelin
2015-12-30Taking into account generated typing constraints in tactic "generalize".Hugo Herbelin
2015-12-30Simplifying code of fourier.Hugo Herbelin
2015-12-30External tactics and notations now accept any tactic argument.Pierre-Marie Pédrot
2015-12-29Fixing bug #4462: unshelve: Anomaly: Uncaught exception Not_found.Pierre-Marie Pédrot
2015-12-28Removing unused parsing entries.Pierre-Marie Pédrot
2015-12-28Implementing non-focussed generic arguments.Pierre-Marie Pédrot
2015-12-28Removing the special status of open_constr generic argument.Pierre-Marie Pédrot
2015-12-28Eradicating uses of open_constr in TACTIC EXTEND in favour of uconstr.Pierre-Marie Pédrot
2015-12-27Factorizing code for untyped constr evaluation.Pierre-Marie Pédrot
2015-12-27Removing dead code.Pierre-Marie Pédrot
2015-12-27Tentative API fix for tactic arguments to be fed to tclWITHHOLES.Pierre-Marie Pédrot
2015-12-25Moving basic generalization tactics upwards for possible use in "intros".Hugo Herbelin
2015-12-25Moving code of specialize so that it can accept "as" (no semantic change).Hugo Herbelin
2015-12-25Moving specialize to Proofview.tactic.Hugo Herbelin
2015-12-25Fixing a bug in the order of side conditions for introduction pattern -> and <-.Hugo Herbelin
2015-12-25Fixing an "injection as" bug in the presence of side conditions.Hugo Herbelin
2015-12-25Moving the ad hoc interpretation of "intros" as "intros **" from tacinterp.mlHugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 03:26:40 +0000