diff options
| author | filliatr | 2000-12-12 22:07:41 +0000 |
|---|---|---|
| committer | filliatr | 2000-12-12 22:07:41 +0000 |
| commit | 8030a420d2cfcf8372d5fe6544efbecde940381b (patch) | |
| tree | 6d4a3c198d4dbecf0cf15f3b53c31447aacfafd7 /proofs | |
| parent | faa2647739aa33421328af4ffeaba1bb474e868e (diff) | |
syntaxe AST Inversion + commentaires ocamlweb autour de $
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1090 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.mli | 2 | ||||
| -rw-r--r-- | proofs/evar_refiner.mli | 2 | ||||
| -rw-r--r-- | proofs/logic.mli | 2 | ||||
| -rw-r--r-- | proofs/pfedit.mli | 2 | ||||
| -rw-r--r-- | proofs/proof_trees.mli | 2 | ||||
| -rw-r--r-- | proofs/proof_type.mli | 2 | ||||
| -rw-r--r-- | proofs/refiner.mli | 2 | ||||
| -rw-r--r-- | proofs/stock.mli | 2 | ||||
| -rw-r--r-- | proofs/tacinterp.mli | 2 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 2 | ||||
| -rw-r--r-- | proofs/tactic_debug.mli | 3 |
11 files changed, 13 insertions, 10 deletions
diff --git a/proofs/clenv.mli b/proofs/clenv.mli index aaf9637f87..05baad0ca1 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (*i*) open Util diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index ac6bc06301..169fde57bf 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (*i*) open Names diff --git a/proofs/logic.mli b/proofs/logic.mli index 1038b5c0d1..8591e33678 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (*i*) open Names diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 0ea35bea94..8b8e41b345 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (*i*) open Pp diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli index c2b73c85d4..043e391702 100644 --- a/proofs/proof_trees.mli +++ b/proofs/proof_trees.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (*i*) open Util diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index 1c1b660773..dbc4ba6554 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (*i*) open Environ diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 68767dc8c1..f359495805 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (*i*) open Term diff --git a/proofs/stock.mli b/proofs/stock.mli index c0cd43c7d5..c08a5b4807 100644 --- a/proofs/stock.mli +++ b/proofs/stock.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (*i*) open Names diff --git a/proofs/tacinterp.mli b/proofs/tacinterp.mli index 800d890517..a23f953e6c 100644 --- a/proofs/tacinterp.mli +++ b/proofs/tacinterp.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (*i*) open Dyn diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index ee80beba8b..a7cf3b6ccc 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (*i*) open Names diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli index 26ab1a9470..fffe583489 100644 --- a/proofs/tactic_debug.mli +++ b/proofs/tactic_debug.mli @@ -1,3 +1,6 @@ + +(*i $Id$ i*) + open Proof_type open Term |