index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
proofs
/
proof_type.mli
Commit message (
Expand
)
Author
Age
*
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-09-27
|
\
|
*
Moving "move" in the new proof engine.
Hugo Herbelin
2016-09-24
*
|
Unplugging Tacexpr in several interface files.
Pierre-Marie Pédrot
2016-09-08
|
/
*
Adding a bit of documentation in the mli.
Pierre-Marie Pédrot
2016-06-09
*
Put the "cofix" tactic in the monad.
Pierre-Marie Pédrot
2016-05-16
*
Put the "fix" tactic in the monad.
Pierre-Marie Pédrot
2016-05-16
*
Put the "clear" tactic into the monad.
Pierre-Marie Pédrot
2016-05-16
*
Moving Ltac traces to Tacexpr and Tacinterp.
Pierre-Marie Pédrot
2016-03-06
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
Removing dead code.
Pierre-Marie Pédrot
2015-02-02
*
Update headers.
Maxime Dénès
2015-01-12
*
Removing useless flag of the historical move tactic.
Pierre-Marie Pédrot
2014-11-22
*
Removing the legacy intro tactic code.
Pierre-Marie Pédrot
2014-11-07
*
Removing the old rename tactic.
Pierre-Marie Pédrot
2014-11-04
*
Removing Convert_concl and Convert_hyp from Logic.
Hugo Herbelin
2014-10-09
*
Fixing localisation of tactic errors (my mistake in himsg.ml essentially).
Hugo Herbelin
2014-09-10
*
Removing the old implementation of clear_body.
Pierre-Marie Pédrot
2014-09-05
*
Revert the two previous commits. I was testing in the wrong branch.
Pierre-Marie Pédrot
2014-09-04
*
Removing the old implementation of clear_body.
Pierre-Marie Pédrot
2014-09-04
*
Removing dead code, thanks to new OCaml warnings and a bit of scripting.
Pierre-Marie Pédrot
2014-04-23
*
Removing the Change_evar refiner rule.
Pierre-Marie Pédrot
2014-03-31
*
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2014-03-05
*
Removing a fishy use of pervasive equality in Ltac backtrace printing.
Pierre-Marie Pédrot
2014-03-01
*
Do not print tactic notation names at each interpretation step.
ppedrot
2013-11-12
*
Generalizing the use of maps instead of lists in the interpretation
ppedrot
2013-06-22
*
Removing a useless location in ltac trace mechanism.
ppedrot
2013-05-30
*
Getting rid of LtacLocated exception transformer.
ppedrot
2013-05-28
*
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-29
*
Embedded exns in LtacLocated and EvaluatedError satisfy Errors.noncritical
letouzey
2013-03-14
*
Revised the Ltac trace mechanism so that trace breaking due to
herbelin
2013-02-17
*
Modulification of identifier
ppedrot
2012-12-14
*
Clean-up : removal of Proof_type.tactic_expr
letouzey
2012-10-06
*
Proof_type: rule now degenerates to prim_rule
letouzey
2012-10-06
*
Clean-up : no more Proof_type.proof_tree
letouzey
2012-10-06
*
Clean-up of proof_type.ml : no more Nested nor abstract_tactic_box
letouzey
2012-10-06
*
Updating headers.
herbelin
2012-08-08
*
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-22
*
Glob_term now mli-only, operations now in Glob_ops
letouzey
2012-05-29
*
Noise for nothing
pboutill
2012-03-02
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
*
Change of nomenclature: rawconstr -> glob_constr
glondu
2010-12-23
*
Remove open_subgoals field of proof_tree
glondu
2010-10-06
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
New script dev/tools/change-header to automatically update Coq files headers.
herbelin
2010-06-22
*
Added support for Ltac-matching terms with variables bound in the pattern
herbelin
2010-06-06
*
Various minor improvements of comments in mli for ocamldoc
letouzey
2010-04-29
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Move from ocamlweb to ocamdoc to generate mli documentation
pboutill
2010-04-29
*
Here comes the commit, announced long ago, of the new tactic engine.
aspiwack
2010-04-22
*
Generic support for open terms in tactics
herbelin
2009-12-21
[next]