X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationMatcher.ml;fp=helm%2Focaml%2Fcic_notation%2FcicNotationMatcher.ml;h=39c82b7dadb66a1e095969c133ff2d9ab23d5078;hb=26cce624c98e795521078794c748758798031704;hp=1a0c024104feaaab9f730ed16c5101c3f72ce965;hpb=f508a0d1a9202186ec9b913ce1ddc6861918ad64;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.ml b/helm/ocaml/cic_notation/cicNotationMatcher.ml
index 1a0c02410..39c82b7da 100644
--- a/helm/ocaml/cic_notation/cicNotationMatcher.ml
+++ b/helm/ocaml/cic_notation/cicNotationMatcher.ml
@@ -277,7 +277,7 @@ struct
 		let env' = Env.remove_names env (List.map fst magic_map) in
 		Some (env', pid)))
         (fun _ -> None)
-        candidates
+        (List.rev candidates)
     in
     let match_cb rows =
       let candidates =
@@ -335,12 +335,9 @@ struct
           | _ -> assert false)
 
     | Pt.If (guard, p) ->
-	prerr_endline ("guard = " ^ CicNotationPp.pp_term guard) ;
-	prerr_endline ("p = " ^ CicNotationPp.pp_term p) ;
 	let compiled_guard = compiler [guard, 0]
 	and compiled_p = compiler [p, 0] in
 	  (fun term env ->
-	     prerr_endline "GUARDIA?" ;
 	     match compiled_guard term with
 	       | None -> None
 	       | Some _ ->
@@ -348,10 +345,23 @@ struct
 		     match compiled_p term with
 		       | None -> None
 		       | Some (env', _) ->
-			   prerr_endline "guardia ok" ;
 			   Some (env' @ env)
 		   end)
 
+    | Pt.Unless (guard, p) ->
+	let compiled_guard = compiler [guard, 0]
+	and compiled_p = compiler [p, 0] in
+	  (fun term env ->
+	     match compiled_guard term with
+	       | None ->
+		   begin
+		     match compiled_p term with
+		       | None -> None
+		       | Some (env', _) ->
+			   Some (env' @ env)
+		   end
+	       | Some _ -> None)
+
     | _ -> assert false
 end