Duplicated exception definition removed (used to give birth to a bug due to

[helm.git] / helm / ocaml / cic_notation / cicNotationParser.ml

diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml
index bcfd6c9f62282e15163a5e988beb3a736702d41a..578a9d6f04ae7d116dbd88f2773d51427c1ab1ff 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationParser.ml
+++ b/helm/ocaml/cic_notation/cicNotationParser.ml
@@ -46,8 +46,6 @@ let term = Grammar.Entry.create level2_ast_grammar "term"
 let let_defs = Grammar.Entry.create level2_ast_grammar "let_defs"
 let level2_meta = Grammar.Entry.create level2_meta_grammar "level2_meta"
 
-let return_term loc term = ()
-
 let int_of_string s =
   try
     Pervasives.int_of_string s
@@ -425,7 +423,7 @@ EXTEND
   sort: [
     [ "Prop" -> `Prop
     | "Set" -> `Set
-    | "Type" -> `Type
+    | "Type" -> `Type (CicUniv.fresh ()) 
     | "CProp" -> `CProp
     ]
   ];