From 420f78b2caeaaddc6fe484565b2d0e49c66888e5 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 27 Jul 2014 10:02:38 +0200 Subject: Imported Upstream version 8.4pl4dfsg --- pretyping/glob_term.ml | 23 +---------------------- 1 file changed, 1 insertion(+), 22 deletions(-) (limited to 'pretyping/glob_term.ml') diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index 8e4b211f..b7023db0 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Anonymous -> - (* Unable to manage the presence of both an alias and a variable *) - raise Not_found - | GVar (loc,id) -> PatVar (loc,Name id) - | GHole (loc,_) -> PatVar (loc,na) - | GRef (loc,ConstructRef cstr) -> - PatCstr (loc,cstr,[],na) - | GApp (loc,GRef (_,ConstructRef (ind,_ as cstr)),args) -> - let mib,_ = Global.lookup_inductive ind in - let nparams = mib.Declarations.mind_nparams in - if nparams > List.length args then - user_err_loc (loc,"",Pp.str "Invalid notation for pattern."); - let params,args = list_chop nparams args in - List.iter (function GHole _ -> () - | _ -> user_err_loc (loc,"",Pp.str"Invalid notation for pattern.")) - params; - let args = List.map (cases_pattern_of_glob_constr Anonymous) args in - PatCstr (loc,cstr,args,na) - | _ -> raise Not_found - let rec cases_pattern_of_glob_constr na = function | GVar (loc,id) when na<>Anonymous -> (* Unable to manage the presence of both an alias and a variable *) -- cgit v1.2.3