1. we compare the expected branching with the actual one and

[helm.git] / matitaB / components / ng_tactics / nDestructTac.ml

diff --git a/matitaB/components/ng_tactics/nDestructTac.ml b/matitaB/components/ng_tactics/nDestructTac.ml
index 0ed800626d762480895d176fefd9020e3a6b9493..ef564afc6dbe7e63823679d338313bd652b0803b 100644 (file)
--- a/matitaB/components/ng_tactics/nDestructTac.ml
+++ b/matitaB/components/ng_tactics/nDestructTac.ml
@@ -41,7 +41,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 mk_prods l t =