From 39cbf75c554cd7e5228bd6cd962766e865c3f26b Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 16 Mar 2017 13:24:03 +0100 Subject: Make some functions on terms more robust w.r.t new term constructs. Extending terms is notoriously difficult. We try to get more help from the compiler by making sure such an extension will trigger non exhaustive pattern matching warnings. --- plugins/extraction/extraction.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/extraction') diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 47e812319..4ae875cd7 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -302,7 +302,7 @@ let rec extract_type env db j c args = if Projection.unfolded p then Tunknown else extract_type env db j (mkProj (Projection.unfold p, t)) args | Case _ | Fix _ | CoFix _ -> Tunknown - | _ -> assert false + | Var _ | Meta _ | Evar _ | Cast _ | LetIn _ | Construct _ -> assert false (*s Auxiliary function dealing with type application. Precondition: [r] is a type scheme represented by the signature [s], -- cgit v1.2.3