]> matita.cs.unibo.it Git - helm.git/blobdiff - matitaB/components/ng_tactics/nInversion.ml
arithmetics for λδ
[helm.git] / matitaB / components / ng_tactics / nInversion.ml
index cf4711db51f25320bcd6664822399e307f0b8662..9319683ed2740fe9f32f414c953f54fee9d1fe48 100644 (file)
@@ -23,7 +23,7 @@ let fresh_name =
 
 let mk_id id =
  let id = if id = "_" then fresh_name () else id in
-  NotationPt.Ident (id,None)
+  NotationPt.Ident (id,`Ambiguous)
 ;;
 
 let rec split_arity status ~subst context te =