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.ml
Commit message (
Expand
)
Author
Age
*
Update headers following #6543.
Théo Zimmermann
2018-02-27
*
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-11-06
*
Merge PR #830: Moving assert (the "Cut" rule) to new proof engine
Maxime Dénès
2017-08-29
|
\
*
|
[api] Put modules in order in API.{mli,ml}
Emilio Jesus Gallego Arias
2017-07-25
|
/
*
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
*
Revised the Ltac trace mechanism so that trace breaking due to
herbelin
2013-02-17
*
Modulification of identifier
ppedrot
2012-12-14
*
still some more dead code removal
letouzey
2012-10-06
*
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
*
Remove some more "open" and dead code thanks to OCaml4 warnings
letouzey
2012-10-02
*
This patch removes unused "open" (automatically generated from
regisgia
2012-09-14
*
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
*
Added support for Ltac-matching terms with variables bound in the pattern
herbelin
2010-06-06
*
Remove the svn-specific $Id$ annotations
letouzey
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
*
Made the interpretation levels rlevel/glevel/tlevel truly phantom
herbelin
2009-12-19
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0
herbelin
2009-06-06
*
Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"
herbelin
2009-03-16
[next]