aboutsummaryrefslogtreecommitdiff
path: root/proofs
AgeCommit message (Expand)Author
2013-03-16another Errors.push in a exception reraiseletouzey
2013-03-14Embedded exns in LtacLocated and EvaluatedError satisfy Errors.noncriticalletouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 12)letouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 5)letouzey
2013-03-12invalid_arg instead of raise (Invalid_argement ...)letouzey
2013-03-12Allowing different types of, not to be mixed, generic Stores throughppedrot
2013-02-18Removing Exc_located and using the new exception enrichementppedrot
2013-02-17Added propagation of evars unification failure reasons for betterherbelin
2013-02-17Revised the Ltac trace mechanism so that trace breaking due toherbelin
2013-01-29No reason a priori for using unfiltered env for printingherbelin
2013-01-29Fixing bug #2969 (admit failing after Grab Existential Variables dueherbelin
2013-01-29Fixed synchronicity of filter with evar context in new_goal_with.herbelin
2013-01-29Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_envherbelin
2013-01-28Actually adding backtrace handling.ppedrot
2013-01-28Uniformization of the "anomaly" command.ppedrot
2013-01-28Added backtrace information to anomaliesppedrot
2013-01-24Reductionops: whd_state_gen can take and answers a cst_stack toopboutill
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
2012-12-21Yet a new reduction tactic in Coq : cbnpboutill
2012-12-18Modulification of nameppedrot
2012-12-18Fixed a little inefficiency of "set/destruct" over a pattern. Nowherbelin
2012-12-14Modulification of identifierppedrot
2012-12-14Moved Stringset and Stringmap to String namespace.ppedrot
2012-12-14Moved Intset and Intmap to Int namespace.ppedrot
2012-12-13Renamed Option.Misc.compare to the more uniform Option.equal.ppedrot
2012-11-25Monomorphization (proof)ppedrot
2012-11-08Monomorphized a lot of equalities over OCaml integers, thanks toppedrot
2012-10-22Fix bug #2892letouzey
2012-10-06still some more dead code removalletouzey
2012-10-06remove Refiner.abstract_tactic and similarletouzey
2012-10-06Clean-up : removal of Proof_type.tactic_exprletouzey
2012-10-06Proof_type: rule now degenerates to prim_ruleletouzey
2012-10-06Clean-up : no more Proof_type.proof_treeletouzey
2012-10-06Clean-up of proof_type.ml : no more Nested nor abstract_tactic_boxletouzey
2012-10-02Remove the unused "intel" field in Proof.proof_stateletouzey
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-10-02Use the library function List.substract in prev commitletouzey
2012-10-01Added a new tactical infoH tac, that displays the names of hypothesis created...courtieu
2012-09-14As r15801: putting everything from Util.array_* to CArray.*.ppedrot
2012-09-14Partial revert of Yann commit in order to use CLib.List when openingppedrot
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-09-14The new ocaml compiler (4.00) has a lot of very cool warnings,regisgia
2012-08-08Updating headers.herbelin
2012-07-20Reductionops refactoringpboutill
2012-07-11Severe reorganisation of the code of tactics in Proofview.aspiwack
2012-07-10Small change in the printing of proofs for use by coqide.aspiwack
2012-07-04Change how the number of open goals is printed.aspiwack
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-06-04Forward-port fixes from 8.4 (15358, 15353, 15333).msozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 00:07:39 +0000