differentieted empty substitution list from no substitution given

[helm.git] / helm / ocaml / cic_transformations / cicAst.ml

diff --git a/helm/ocaml/cic_transformations/cicAst.ml b/helm/ocaml/cic_transformations/cicAst.ml
index 92ab328c18a1e9ac16881d5d7815da2664cd9a68..f7392fa3ac34bdfe8c4423902cd54a4c4c15fb06 100644 (file)
--- 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 *)