* implemented unless

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

diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.ml b/helm/ocaml/cic_notation/cicNotationMatcher.ml
index 1a0c024104feaaab9f730ed16c5101c3f72ce965..39c82b7dadb66a1e095969c133ff2d9ab23d5078 100644 (file)
--- 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