- Procedural: we now check that an eliminator opens as many goals as the ...

[helm.git] / helm / software / components / acic_content / cicNotationEnv.ml

diff --git a/helm/software/components/acic_content/cicNotationEnv.ml b/helm/software/components/acic_content/cicNotationEnv.ml
index 32d4f0df5e699043505022a31d48d3baa91a7d82..f0a14846f2e934610f9e2f36b1df6e93e6d96036 100644 (file)
--- a/helm/software/components/acic_content/cicNotationEnv.ml
+++ b/helm/software/components/acic_content/cicNotationEnv.ml
@@ -35,7 +35,7 @@ type value =
   | ListValue of value list
 
 type value_type =
-  | TermType
+  | TermType of int option
   | StringType
   | NumType
   | OptType of value_type
@@ -98,7 +98,7 @@ let list_declaration (n, ty) = (n, ListType ty)
 let declaration_of_var = function
   | Ast.NumVar s -> s, NumType
   | Ast.IdentVar s -> s, StringType
-  | Ast.TermVar s -> s, TermType
+  | Ast.TermVar (s,l) -> s, TermType l
   | _ -> assert false
 
 let value_of_term = function
@@ -114,7 +114,7 @@ let term_of_value = function
 
 let rec well_typed ty value =
   match ty, value with
-  | TermType, TermValue _
+  | TermType _, TermValue _
   | StringType, StringValue _
   | OptType _, OptValue None
   | NumType, NumValue _ -> true