diff options
Diffstat (limited to 'pretyping/glob_term.ml')
| -rw-r--r-- | pretyping/glob_term.ml | 23 |
1 files changed, 1 insertions, 22 deletions
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 *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -359,27 +359,6 @@ let rec cases_pattern_of_glob_constr na = function 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 *) - 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 - (* Turn a closed cases pattern into a glob_constr *) let rec glob_constr_of_closed_cases_pattern_aux = function | PatCstr (loc,cstr,[],Anonymous) -> |