X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FcicAst.ml;h=f7392fa3ac34bdfe8c4423902cd54a4c4c15fb06;hb=c5d5bf37b1e4c4b9b499ed2cbfe27cf2ec181944;hp=92ab328c18a1e9ac16881d5d7815da2664cd9a68;hpb=9e4d691ac9e6edb63703a9e4e49b02c86b38624e;p=helm.git

diff --git a/helm/ocaml/cic_transformations/cicAst.ml b/helm/ocaml/cic_transformations/cicAst.ml
index 92ab328c1..f7392fa3a 100644
--- a/helm/ocaml/cic_transformations/cicAst.ml
+++ b/helm/ocaml/cic_transformations/cicAst.ml
@@ -44,7 +44,10 @@ type term =
   | LetIn of capture_variable * term * term  (* name, body, where *)
   | LetRec of induction_kind * (capture_variable * term * int) list * term
       (* (name, body, decreasing argument) list, where *)
-  | Ident of string * subst list  (* literal, substitutions *)
+  | Ident of string * subst list option
+      (* literal, substitutions.
+      * Some [] -> user has given an empty explicit substitution list 
+      * None -> user has given no explicit substitution list *)
   | Implicit
   | Meta of int * meta_subst list
   | Num of string * int (* literal, instance *)