unification:

[helm.git] / helm / software / components / ng_refiner / nCicRefiner.ml

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 7871d86e92052728a1828627783c0c83642fec24..8c5dcae76d0d700e5a93156faa32bdb5eae66ba0 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -309,7 +309,7 @@ let rec typeof hdb
       let resty = C.Appl (outtype::arguments@[term]) in
       let resty = NCicReduction.head_beta_reduce ~subst resty in
       metasenv, subst, C.Match (r, outtype, term, List.rev pl_rev),resty
-    | C.Match _ as orig -> assert false
+    | C.Match _ -> assert false
     in
     pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t ^ " :: "^
          NCicPp.ppterm ~metasenv ~subst ~context infty ));
@@ -586,7 +586,7 @@ let typeof_obj hdb
        uri, height, metasenv, subst, 
          C.Fixpoint (inductive, fl, attr)
 
-  | C.Inductive (ind, leftno, itl, attr) ->  assert false
+  | C.Inductive (_ind, _leftno, _itl, _attr) ->  assert false
 (*
   (* let's check if the arity of the inductive types are well formed *)
   List.iter (fun (_,_,x,_) -> ignore (typeof ~subst ~metasenv [] x)) tyl;