X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2Fcic.ml;h=c997d99ca3d3a866fbed691f1929803f46149b8c;hb=ac7687ce66526f905874ed99a845223c853c558a;hp=f9e99260d52944640d65ace9d5d9b6909be8cd42;hpb=c5d5bf37b1e4c4b9b499ed2cbfe27cf2ec181944;p=helm.git

diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml
index f9e99260d..c997d99ca 100644
--- a/helm/ocaml/cic/cic.ml
+++ b/helm/ocaml/cic/cic.ml
@@ -23,17 +23,17 @@
  * http://cs.unibo.it/helm/.
  *)
 
-(******************************************************************************)
-(*                                                                            *)
-(*                               PROJECT HELM                                 *)
-(*                                                                            *)
-(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
-(*                                 29/11/2000                                 *)
-(*                                                                            *)
-(* This module defines the internal representation of the objects (variables, *)
-(* blocks of (co)inductive definitions and constants) and the terms of cic    *)
-(*                                                                            *)
-(******************************************************************************)
+(*****************************************************************************)
+(*                                                                           *)
+(*                               PROJECT HELM                                *)
+(*                                                                           *)
+(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>              *)
+(*                                 29/11/2000                                *)
+(*                                                                           *)
+(* This module defines the internal representation of the objects (variables,*)
+(* blocks of (co)inductive definitions and constants) and the terms of cic   *)
+(*                                                                           *)
+(*****************************************************************************)
 
 (* STUFF TO MANAGE IDENTIFIERS *)
 type id = string  (* the abstract type of the (annotated) node identifiers *)
@@ -110,6 +110,9 @@ and coInductiveFun =
 (* depend on new ones.                                           *)
 and conjecture = int * context * term
 and metasenv = conjecture list
+and substitution = (int * (context * term * term)) list
+
+
 
 (* a metasenv is a list of declarations of metas in declarations *)
 (* order (i.e. [oldest ; ... ; newest]). Older variables can not *)