X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=50a0c59da2da3973feffe89da6ee7451575e9e98;hb=4573f1fecaf83f4706f39702555d5319d132477b;hp=b49af2bbf5999b69f693293c5bb7f7a462345487;hpb=7bc72d8afaebb1d2070a26b07f9bf4242b648e2c;p=helm.git

diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
index b49af2bbf..50a0c59da 100644
--- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
@@ -304,7 +304,7 @@ let interpretate_term_and_interpretate_term_option
         in
         let cic_body = aux ~localize loc (cic_name :: context) body in
         NCic.LetIn (cic_name, cic_typ, cic_def, cic_body)
-    | CicNotationPt.LetRec (_kind, _defs, _body) -> assert false 
+    | CicNotationPt.LetRec (_kind, _defs, _body) -> NCic.Implicit `Term
     | CicNotationPt.Ident _
     | CicNotationPt.Uri _ when is_path -> raise Disambiguate.PathNotWellFormed
     | CicNotationPt.Ident (name, subst) ->